Forward refinement for dynamic concurrent processes

This file introduces the first process-level refinement notion for the dynamic concurrent core.

The central object is ForwardSimulation between two Process.Systems. It captures the usual implementation/specification picture:

• implementation and specification states are related by a simulation invariant;
• every admissible implementation start state can be matched by some specification start state;
• every concrete implementation step can be simulated by a specification step;
• the simulation may additionally insist that the two steps agree on events, tickets, controller data, or local observations; and
• safety obligations may be transferred from the specification side back to the implementation side.

This gives a reusable refinement layer that is independent of any particular concurrent frontend and rich enough to support observational reasoning, not just state-reachability arguments.

structure Interaction.Concurrent.Refinement.ForwardSimulation {Γ : Spec.Node.Context} {Δ : Spec.Node.Context} (impl : ProcessOver.System Γ) (spec : ProcessOver.System Δ) (matchStep : impl.TranscriptRel spec.toProcess := fun {pL : impl.Proc} {pR : spec.Proc} => ProcessOver.TranscriptRel.top) : Type (max u_1 u_2)

ForwardSimulation impl spec matchStep is a forward simulation from the implementation system impl to the specification system spec.

The meaning is:

• every initial implementation state is related to some initial specification state;
• assumptions are preserved from implementation to specification;
• every implementation step transcript can be matched by some specification step transcript satisfying matchStep;
• related safe specification states imply safe implementation states.

This is intentionally phrased over the dynamic Process.System core rather than any particular concurrent frontend.

The parameter matchStep determines what behavioral information the simulation preserves at each step. Choosing different transcript relations recovers event-preserving, ticket-preserving, controller-preserving, or observation-preserving refinements.

• stateRel : impl.Proc → spec.Proc → Prop
• init (pImpl : impl.Proc) : impl.init pImpl → ∃ (pSpec : spec.Proc), spec.init pSpec ∧ self.stateRel pImpl pSpec
• assumptions {pImpl : impl.Proc} {pSpec : spec.Proc} : self.stateRel pImpl pSpec → impl.assumptions pImpl → spec.assumptions pSpec
• step {pImpl : impl.Proc} {pSpec : spec.Proc} : self.stateRel pImpl pSpec → ∀ (trImpl : (impl.step pImpl).spec.Transcript), ∃ (trSpec : (spec.step pSpec).spec.Transcript), matchStep trImpl trSpec ∧ self.stateRel ((impl.step pImpl).next trImpl) ((spec.step pSpec).next trSpec)
• safe {pImpl : impl.Proc} {pSpec : spec.Proc} : self.stateRel pImpl pSpec → spec.safe pSpec → impl.safe pImpl

noncomputable def Interaction.Concurrent.Refinement.ForwardSimulation.matchTranscript {Γ : Spec.Node.Context} {Δ : Spec.Node.Context} {impl : ProcessOver.System Γ} {spec : ProcessOver.System Δ} {matchStep : impl.TranscriptRel spec.toProcess} (sim : ForwardSimulation impl spec fun {pL : impl.Proc} {pR : spec.Proc} => matchStep) {pImpl : impl.Proc} {pSpec : spec.Proc} (hrel : sim.stateRel pImpl pSpec) (trImpl : (impl.step pImpl).spec.Transcript) : (spec.step pSpec).spec.Transcript

Choose the matching specification transcript for one implementation transcript.

This is the specification-side step selected by the simulation for the given implementation step.

theorem Interaction.Concurrent.Refinement.ForwardSimulation.matchTranscript_spec {Γ : Spec.Node.Context} {Δ : Spec.Node.Context} {impl : ProcessOver.System Γ} {spec : ProcessOver.System Δ} {matchStep : impl.TranscriptRel spec.toProcess} (sim : ForwardSimulation impl spec fun {pL : impl.Proc} {pR : spec.Proc} => matchStep) {pImpl : impl.Proc} {pSpec : spec.Proc} (hrel : sim.stateRel pImpl pSpec) (trImpl : (impl.step pImpl).spec.Transcript) : matchStep trImpl (sim.matchTranscript hrel trImpl) ∧ sim.stateRel ((impl.step pImpl).next trImpl) ((spec.step pSpec).next (sim.matchTranscript hrel trImpl))

The chosen matching transcript satisfies matchStep and preserves the state relation to the next residual states.

noncomputable def Interaction.Concurrent.Refinement.ForwardSimulation.matchedState {Γ : Spec.Node.Context} {Δ : Spec.Node.Context} {impl : ProcessOver.System Γ} {spec : ProcessOver.System Δ} {matchStep : impl.TranscriptRel spec.toProcess} (sim : ForwardSimulation impl spec fun {pL : impl.Proc} {pR : spec.Proc} => matchStep) (run : impl.Run) {pSpec : spec.Proc} (hrel : sim.stateRel run.initial pSpec) (n : ℕ) : { qSpec : spec.Proc // sim.stateRel (run.state n) qSpec }

matchedState sim run hrel n is the specification-side state reached after matching the first n steps of the implementation run run, starting from an initial related specification state witnessed by hrel.

This is the fundamental state-transport construction behind run-level refinement: it recursively follows the implementation run while using the simulation to pick matching specification transcripts.

noncomputable def Interaction.Concurrent.Refinement.ForwardSimulation.matchedTranscript {Γ : Spec.Node.Context} {Δ : Spec.Node.Context} {impl : ProcessOver.System Γ} {spec : ProcessOver.System Δ} {matchStep : impl.TranscriptRel spec.toProcess} (sim : ForwardSimulation impl spec fun {pL : impl.Proc} {pR : spec.Proc} => matchStep) (run : impl.Run) {pSpec : spec.Proc} (hrel : sim.stateRel run.initial pSpec) (n : ℕ) : (spec.step ↑(sim.matchedState run hrel n)).spec.Transcript

The specification transcript chosen to match the nth implementation step of the run run, relative to the initial related specification state witnessed by hrel.

This is the stepwise witness used to build the whole matched specification run.

noncomputable def Interaction.Concurrent.Refinement.ForwardSimulation.mapRun {Γ : Spec.Node.Context} {Δ : Spec.Node.Context} {impl : ProcessOver.System Γ} {spec : ProcessOver.System Δ} {matchStep : impl.TranscriptRel spec.toProcess} (sim : ForwardSimulation impl spec fun {pL : impl.Proc} {pR : spec.Proc} => matchStep) (run : impl.Run) {pSpec : spec.Proc} (hrel : sim.stateRel run.initial pSpec) : spec.Run

mapRun sim run hrel is the specification run obtained by recursively matching every step of the implementation run run, starting from an initial related specification state witnessed by hrel.

So mapRun turns a forward simulation into an execution-level translation from implementation runs to matching specification runs.

theorem Interaction.Concurrent.Refinement.ForwardSimulation.stateRel_mapRun {Γ : Spec.Node.Context} {Δ : Spec.Node.Context} {impl : ProcessOver.System Γ} {spec : ProcessOver.System Δ} {matchStep : impl.TranscriptRel spec.toProcess} (sim : ForwardSimulation impl spec fun {pL : impl.Proc} {pR : spec.Proc} => matchStep) (run : impl.Run) {pSpec : spec.Proc} (hrel : sim.stateRel run.initial pSpec) (n : ℕ) : sim.stateRel (run.state n) ((sim.mapRun run hrel).state n)

At every step index n, the mapped specification run remains related to the implementation run by stateRel.

theorem Interaction.Concurrent.Refinement.ForwardSimulation.match_mapRun {Γ : Spec.Node.Context} {Δ : Spec.Node.Context} {impl : ProcessOver.System Γ} {spec : ProcessOver.System Δ} {matchStep : impl.TranscriptRel spec.toProcess} (sim : ForwardSimulation impl spec fun {pL : impl.Proc} {pR : spec.Proc} => matchStep) (run : impl.Run) {pSpec : spec.Proc} (hrel : sim.stateRel run.initial pSpec) (n : ℕ) : matchStep (run.transcript n) ((sim.mapRun run hrel).transcript n)

At every step index n, the mapped specification transcript matches the implementation transcript by matchStep.

This is the run-level form of the step-matching guarantee.

theorem Interaction.Concurrent.Refinement.ForwardSimulation.safe_of_mapRun {Γ : Spec.Node.Context} {Δ : Spec.Node.Context} {impl : ProcessOver.System Γ} {spec : ProcessOver.System Δ} {matchStep : impl.TranscriptRel spec.toProcess} (sim : ForwardSimulation impl spec fun {pL : impl.Proc} {pR : spec.Proc} => matchStep) (run : impl.Run) {pSpec : spec.Proc} (hrel : sim.stateRel run.initial pSpec) (hsafe : ∀ (n : ℕ), spec.safe ((sim.mapRun run hrel).state n)) (n : ℕ) : impl.safe (run.state n)

If every state along the mapped specification run is safe, then every state along the implementation run is safe.

This is the basic safety-transport principle of forward simulation.

theorem Interaction.Concurrent.Refinement.ForwardSimulation.admissible_mapRun {Γ : Spec.Node.Context} {Δ : Spec.Node.Context} {impl : ProcessOver.System Γ} {spec : ProcessOver.System Δ} {matchStep : impl.TranscriptRel spec.toProcess} (sim : ForwardSimulation impl spec fun {pL : impl.Proc} {pR : spec.Proc} => matchStep) (run : impl.Run) {pSpec : spec.Proc} (hrel : sim.stateRel run.initial pSpec) (hadm : impl.Admissible run) : spec.Admissible (sim.mapRun run hrel)

If an implementation run is admissible, then its mapped specification run is also admissible.

So ambient assumptions are preserved along the run translation induced by the simulation.

theorem Interaction.Concurrent.Refinement.ForwardSimulation.prefixRel_mapRun {Γ : Spec.Node.Context} {Δ : Spec.Node.Context} {impl : ProcessOver.System Γ} {spec : ProcessOver.System Δ} {matchStep : impl.TranscriptRel spec.toProcess} (sim : ForwardSimulation impl spec fun {pL : impl.Proc} {pR : spec.Proc} => matchStep) (run : impl.Run) {pSpec : spec.Proc} (hrel : sim.stateRel run.initial pSpec) (n : ℕ) : ProcessOver.Run.RelUpTo (fun {pL : impl.Proc} {pR : spec.Proc} => matchStep) run (sim.mapRun run hrel) n

The first n steps of the mapped specification run match the first n implementation steps according to matchStep.

theorem Interaction.Concurrent.Refinement.ForwardSimulation.runRel_mapRun {Γ : Spec.Node.Context} {Δ : Spec.Node.Context} {impl : ProcessOver.System Γ} {spec : ProcessOver.System Δ} {matchStep : impl.TranscriptRel spec.toProcess} (sim : ForwardSimulation impl spec fun {pL : impl.Proc} {pR : spec.Proc} => matchStep) (run : impl.Run) {pSpec : spec.Proc} (hrel : sim.stateRel run.initial pSpec) : ProcessOver.Run.Rel (fun {pL : impl.Proc} {pR : spec.Proc} => matchStep) run (sim.mapRun run hrel)

The mapped specification run matches the implementation run at every finite prefix according to matchStep.

theorem Interaction.Concurrent.Refinement.ForwardSimulation.currentControllersUpTo_mapRun {Party : Type u} {impl : Process.System Party} {spec : Process.System Party} (sim : ForwardSimulation impl spec fun {pL : impl.Proc} {pR : spec.Proc} => Observation.Process.TranscriptRel.byController) (run : Process.Run impl.toProcess) {pSpec : spec.Proc} (hrel : sim.stateRel run.initial pSpec) (n : ℕ) : run.currentControllersUpTo n = Process.Run.currentControllersUpTo (sim.mapRun run hrel) n

A controller-preserving simulation preserves the current controller sequence of every finite run prefix.

theorem Interaction.Concurrent.Refinement.ForwardSimulation.controllerPathsUpTo_mapRun {Party : Type u} {impl : Process.System Party} {spec : Process.System Party} (sim : ForwardSimulation impl spec fun {pL : impl.Proc} {pR : spec.Proc} => Observation.Process.TranscriptRel.byPath) (run : Process.Run impl.toProcess) {pSpec : spec.Proc} (hrel : sim.stateRel run.initial pSpec) (n : ℕ) : run.controllerPathsUpTo n = Process.Run.controllerPathsUpTo (sim.mapRun run hrel) n

A controller-path-preserving simulation preserves the controller-path sequence of every finite run prefix.

theorem Interaction.Concurrent.Refinement.ForwardSimulation.eventsUpTo_mapRun {Party : Type u} {impl : Process.System Party} {spec : Process.System Party} {Event : Type w} {eventImpl : impl.EventMap Event} {eventSpec : spec.EventMap Event} (sim : ForwardSimulation impl spec fun {pL : impl.Proc} {pR : spec.Proc} => Observation.Process.TranscriptRel.byEvent eventImpl eventSpec) (run : Process.Run impl.toProcess) {pSpec : spec.Proc} (hrel : sim.stateRel run.initial pSpec) (n : ℕ) : Process.Run.eventsUpTo eventImpl run n = Process.Run.eventsUpTo eventSpec (sim.mapRun run hrel) n

An event-preserving simulation preserves the stable event sequence of every finite run prefix.

theorem Interaction.Concurrent.Refinement.ForwardSimulation.ticketsUpTo_mapRun {Party : Type u} {impl : Process.System Party} {spec : Process.System Party} {Ticket : Type w} {ticketImpl : impl.Tickets Ticket} {ticketSpec : spec.Tickets Ticket} (sim : ForwardSimulation impl spec fun {pL : impl.Proc} {pR : spec.Proc} => Observation.Process.TranscriptRel.byTicket ticketImpl ticketSpec) (run : Process.Run impl.toProcess) {pSpec : spec.Proc} (hrel : sim.stateRel run.initial pSpec) (n : ℕ) : Process.Run.ticketsUpTo ticketImpl run n = Process.Run.ticketsUpTo ticketSpec (sim.mapRun run hrel) n

A ticket-preserving simulation preserves the stable ticket sequence of every finite run prefix.

theorem Interaction.Concurrent.Refinement.ForwardSimulation.observationsUpTo_mapRun {Party : Type u} [DecidableEq Party] (me : Party) {impl : Process.System Party} {spec : Process.System Party} (sim : ForwardSimulation impl spec fun {pL : impl.Proc} {pR : spec.Proc} => Observation.Process.TranscriptRel.byObservation me) (run : Process.Run impl.toProcess) {pSpec : spec.Proc} (hrel : sim.stateRel run.initial pSpec) (n : ℕ) : Observation.Process.Run.observationsUpTo me run n = Observation.Process.Run.observationsUpTo me (sim.mapRun run hrel) n

An observation-preserving simulation preserves one party's packed observations of every finite run prefix.

theorem Interaction.Concurrent.Refinement.ForwardSimulation.safe_of_satisfies {Γ : Spec.Node.Context} {Δ : Spec.Node.Context} {impl : ProcessOver.System Γ} {spec : ProcessOver.System Δ} {matchStep : impl.TranscriptRel spec.toProcess} (sim : ForwardSimulation impl spec fun {pL : impl.Proc} {pR : spec.Proc} => matchStep) (fairImpl : ProcessOver.Run.Pred impl.toProcess) (fairSpec : ProcessOver.Run.Pred spec.toProcess) (hfair : ∀ (run : impl.Run) {pSpec : spec.Proc} (hrel : sim.stateRel run.initial pSpec), fairImpl run → fairSpec (sim.mapRun run hrel)) (hspec : spec.Satisfies fairSpec spec.Safe) : impl.Satisfies fairImpl impl.Safe

If the specification system satisfies safety under some fairness assumption, then the implementation system also satisfies safety under any implementation fairness assumption that transfers along the simulation.

This is the top-level preservation theorem: once fairness is known to transfer, forward simulation lets one discharge implementation-side safety obligations by proving them on the specification side.