lf-lang / reactor-model Goto Github PK

https://github.com/marcusrossel/reactor-model/blob/809d7063f7d9a907f751a57b9e3311955ef58fcd/src/primitives.lean

On branch physical.

I think we can more or less easily extend the formalization with physical actions.

We will probably need to:

• Add a Component.phy (and rename Component.act to Component.log).
• Add an execution step which handles physical events and can always be taken (figure out the precise semantics for this first though).
• We may also have to add wall clock time to Execution.State.

Can we still show execution to be deterministic if the physical actions occur at the same wall clock times across executions?

cf. Marten's dissertation page 67

... as a mutually inductive definition of:

• mutation-output
• mutation
• reaction (as extension of mutation)
• reactor
• network

I think it might be realistic to attempt connecting (a rewritten version of) the Lean target with this formalization.
The target's reactor type would be shown to conform to Reactor.Proper. The target's runtime can probably be implemented such that we have a function time for a time step, a function skip for a skip step and a function exec for an execution step, with them being combined into a single step function which determines which step to take and calls it. We would then need to prove something like ∀ s, s ↓ (step s). Note that this is just an implication and not an equivalence because it captures the notion of refinement. That is, the concrete implementation of the Lean target does not have to (and in fact can't) support all non-deterministic step choices allowed by the Reactor model. Note that this whole approach probably works only when all reactions in the system are pure, i.e. do not support IO.

To then connect with the transitive step relation, we could perhaps define a bounded run function that takes the maximum number of steps as input. Then we would try to prove ∀ n s, s ⇓ (boundedrun n s).

Adjustments of the Formalization

I think to perform the steps outlined above, we would need to adjust the formalization in the following ways:

• Make ID and Value type parameters in or on Reactor. Note that when showing that the Lean target's reactor type conforms to Reactor we would probably set the ID type to be the sum type of all target-native ID-types and the Value type to be the type Σ type : Type, type.
• Make Reaction a type class instance with Priority as a type parameter in or on it.
• Make Execution.State a type class.
• Make Time and Time.Tag a type class.

Note that if you combine the Lean target and the formalization, you can use all of the types declared in the formalization as part of the implementation. But if you want to use a different type for the implementation, you need to have the formalization use a type class for it.

Open Questions

• How can we lift the progress theorem?

In Mathlib.lean.