Computation Thread Module

Exploratory work.

Computation Threads Actions

We have something like: Init -> (Continue+|Cancel)* -> (Success | Cancel) ^ -> + q: Can we init in a success state? I think we should not.

inductive ComputationThreads.Actions.Instruction (β : Type) : Type

• Step {β : Type} : β → Instruction β
• End {β : Type} : Instruction β

inductive ComputationThreads.Actions.Event (α : Type) : Type

• Init {α : Type} (fp_catalogue : Tokens.Elem.TId) (fp_cat_id : ℕ) (fraud_node : Tokens.Elem.TId) : Event α
• Continue {α : Type} (comp_thread : Tokens.Elem.TId) (i : Instruction α) : Event α
• Cancel {α : Type} (compu_thread : Tokens.Elem.TId) : Event α

State

We have the relation and its computational counterpart

Relation

structure ComputationThreads.State.RelState (α β : Type) : Type

• threads : Datum.ComputationThreads α β
• fpTokens : FraudProofTokens.State.FraudProofTokens

def ComputationThreads.State.RelState.init {α β : Type} : RelState α β

Equations

• ComputationThreads.State.RelState.init = { threads := Tokens.State.Tokens.init, fpTokens := Tokens.State.Tokens.init }

inductive ComputationThreads.State.Relation {α β : Type} (c : ℕ → Option (List (α → β → Option (Datum.ComputationState α)))) (stQueue : StateQueue.State.StateQueue) (i : InputInfo) (st : RelState α β) : Actions.Event β → RelState α β → Prop

• Init {α β : Type} {c : ℕ → Option (List (α → β → Option (Datum.ComputationState α)))} {stQueue : StateQueue.State.StateQueue} {i : InputInfo} {st : RelState α β} (fp_cat fraud_node : Tokens.Elem.TId) (fp_cat_id : ℕ) (script : List (α → β → Option (Datum.ComputationState α))) (s' : Datum.ComputationThreads α β) (name : String) : c fp_cat_id = some script → Tokens.State.Tokens.get_name fraud_node stQueue = some name → Relation c stQueue i st (Actions.Event.Init fp_cat fp_cat_id fraud_node) { threads := s', fpTokens := st.fpTokens }
• ContinueNLast {α β : Type} {c : ℕ → Option (List (α → β → Option (Datum.ComputationState α)))} {stQueue : StateQueue.State.StateQueue} {i : InputInfo} {st : RelState α β} (comp_thread : Tokens.Elem.TId) (step : α → β → Option (Datum.ComputationState α)) (thread : Tokens.Elem.TokenD (Datum.Thread α β)) (cs_st : α) (cs_st' : Datum.ComputationState α) (threads' : Tokens.State.Tokens (Datum.Thread α β)) (input : β) : Tokens.State.Tokens.get comp_thread st.threads = some thread → thread.data.datum.data = Datum.ComputationState.State cs_st → step cs_st input = some cs_st' → Tokens.State.Tokens.update_data comp_thread (fun (x : Datum.Thread α β) => let __src := thread.data; { datum := let __src := __src.datum; { fraud_prover := __src.fraud_prover, block_id := __src.block_id, data := cs_st', name := __src.name }, steps := thread.data.steps.tail }) st.threads = some threads' → Relation c stQueue i st (Actions.Event.Continue comp_thread (Actions.Instruction.Step input)) { threads := threads', fpTokens := st.fpTokens }
• ContinueLast {α β : Type} {c : ℕ → Option (List (α → β → Option (Datum.ComputationState α)))} {stQueue : StateQueue.State.StateQueue} {i : InputInfo} {st : RelState α β} (comp_thread : Tokens.Elem.TId) (s' : Datum.ComputationThreads α β) (tokens : FraudProofTokens.State.FraudProofTokens) (comp_token : Tokens.Elem.TokenD (Datum.Thread α β)) : Tokens.State.Tokens.get comp_thread st.threads = some comp_token → comp_token.data.datum.data = Datum.ComputationState.Empty → Relation c stQueue i st (Actions.Event.Continue comp_thread Actions.Instruction.End) { threads := s', fpTokens := tokens }
• Cancel {α β : Type} {c : ℕ → Option (List (α → β → Option (Datum.ComputationState α)))} {stQueue : StateQueue.State.StateQueue} {i : InputInfo} {st : RelState α β} (comp_thread : Tokens.Elem.TId) (s' : Datum.ComputationThreads α β) (comp_token : Tokens.Elem.TokenD (Datum.Thread α β)) : Tokens.State.Tokens.burn comp_thread st.threads = some s' → Tokens.State.Tokens.get comp_thread st.threads = some comp_token → comp_token.data.datum.fraud_prover = i.validator → Relation c stQueue i st (Actions.Event.Cancel comp_thread) { threads := s', fpTokens := st.fpTokens }

Computation