Observation equivalence for concurrent processes #
This file packages the notion of "what a party can tell apart" from concrete executions of a concurrent process.
The process semantics keeps the exact dependent type of each local observation, which is ideal when reasoning inside one fixed execution. But comparison across different executions, processes, or refinement layers needs a uniform carrier. The solution adopted here is to pack each local observation together with its type and then compare executions through these packed observations.
The resulting API provides:
- packed local observations for one sequential step;
- per-step observation summaries for finite traces, finite prefixes, and runs;
- generic transcript relations saying when two executions match; and
- reusable lemmas showing that controller, event, ticket, and observation data are preserved when those transcript relations hold.
This is the comparison layer later used by refinement and equivalence results.
PackedObs is a locally observed value packaged together with its observation
type.
This is the simplest uniform carrier for local observations whose precise type may vary from one visited node to the next.
Instances For
Forget the dependent indices of an observed sequential transcript and keep only the concrete packed sequence of observations that was exposed locally.
This is the uniform, comparison-friendly summary of what one party learned from one complete sequential step transcript.
Instances For
obsList me step tr is the packed sequence of local observations available to
the fixed party me while the sequential process step step executes along
the transcript tr.
This forgets the exact dependent observation types but keeps their concrete values in order, which makes it the basic comparison object for one process step.
Instances For
The per-step packed local observations exposed along a finite complete process trace.
Each list element corresponds to one executed process step and stores the local
observations that me obtained during that step.
Instances For
The per-step packed local observations exposed along a finite process prefix.
This is the prefix-level analogue of Trace.observations.
Instances For
Rel rel left right states that the two finite prefixes left and right
match step-by-step according to the transcript relation rel.
The length index forces the two prefixes to have the same number of executed steps.
So Prefix.Rel is the generic finite-horizon comparison interface: the caller
chooses what it means for one process step of left to match one process step
of right, and Rel lifts that choice to whole finite prefixes.
Instances For
Transporting both prefixes along equal start states does not change their matching relation.
TranscriptRel left right is a cross-process relation on one complete process
step transcript of left and one complete process step transcript of right.
This is the basic matching interface used later by refinement, equivalence, and observation-preservation theorems.
Instances For
The permissive transcript relation that accepts every pair of transcripts.
Instances For
Conjunction of transcript relations.
This is useful when one refinement should preserve several observational features at once.
Instances For
Match two transcripts by equality of their current controlling parties.
Instances For
Match two transcripts by equality of their full controller paths.
Instances For
Match two transcripts by equality of stable external event labels.
Instances For
Match two transcripts by equality of stable tickets.
Instances For
Match two transcripts by equality of the packed local observations exposed to one fixed party.
This is the relation that identifies executions that are observationally
indistinguishable to me at the step level.
Instances For
Matching by current controller equality preserves the extracted controller sequence of finite prefixes.
Matching by controller-path equality preserves the extracted controller path sequence of finite prefixes.
Matching by stable event equality preserves the extracted event sequence of finite prefixes.
Matching by stable ticket equality preserves the extracted ticket sequence of finite prefixes.
Matching by local observation equality preserves the packed observation sequence of finite prefixes for the chosen party.
The per-step packed local observations exposed along the first n steps of the
run run.
This is the infinite-run analogue of Prefix.observations, truncated to the
first n steps.
Instances For
RelUpTo rel left right n states that the first n executed steps of the
runs left and right match step-by-step according to rel.
This is the finite-prefix comparison predicate for runs.
Instances For
Rel rel left right states that every finite prefix of the runs left and
right matches according to rel.
So two runs are related when they remain indistinguishable at every finite horizon under the chosen step-matching criterion.
Instances For
Pointwise transcript matching implies prefix matching of the first n
steps.
Pointwise transcript matching implies full run matching.
Matching by current controller equality preserves the extracted controller
sequence of the first n run steps.
Matching by controller-path equality preserves the extracted controller-path
sequence of the first n run steps.
Matching by stable event equality preserves the extracted event sequence of
the first n run steps.
Matching by stable ticket equality preserves the extracted ticket sequence
of the first n run steps.
Matching by local observation equality preserves the packed observation
sequence of the first n run steps for the chosen party.