A Mechanised Axiomatic Model for Behaviour-Oriented Concurrency

This repo contains the Lean mechanisation accompanying the paper "When Behaviours Have to Happen: An Axiomatic Model of Causality in Behaviour-Oriented Concurrency" (under submission). The mechanisation relies on MathLib for relations and sets. Below is a table containing the mapping from the paper definitions to the corresponding mechanisation.

In the paper	In the mechanisation
BId ($i$)	def BId
CId ($c$)	def Cown
Events ($S_i$/ $R_i$/ $C_i$)	inductive Event
Definition 4 (Structure of BoC executions)	structure Execution (A)
Definition 5 (Derived relations)	def derived_run_relation and def derived_co_any (B)
Definition 6 (Cowns)	let cowns bid := ...
Definition 7 (Happens-before)	def derived_hb_relation
Definition 8 (Valid execution)	structure Execution.valid (C)
$H$ (Figure 8)	structure History
$s$ (Figure 8)	inductive Stmt
$b$ (Figure 8)	structure Behavior
$cfg$ (Figure 8)	structure Cfg
Figure 9	inductive StepBehavior and inductive StepCfg
$\vdash_b$ (Figure 10)	def wf_behavior_history
$\vdash_c$ (Figure 10)	def wf_cown_history
Definition 10 (Well-timed history)	structure History.timestamp_wf
Definition 11 (Well-formed history)	structure History.wf
Definition 12 (Translation to axiomatic model)	def model_from_history
Theorem 13 (Translation soundness)	theorem model_from_history_valid
Definition 14 (Matching history)	structure CfgHistoryInv (D)
Theorem 15 (Preservation of well-formed and matching histories)	theorem wf_preservation

• (A) Items 5 and 6 are defined as part of wf_po_relation and wf_co_relation respectively, which are included in Execution.valid.
• (B) The $\text{co}_c$ relation is expressed as a partial application of $\text{co}$.
• (C) Items 1 (po part), 2, 3, 4 and 5 are defined as part of wf_po_relation. Items 1 (co part), 6 and 7 are defined as part of wf_co_relation
• (D) Item 1 is expressed as pairwise inequality in cfgWf. Remaining items are in historyMatches

The mechanisation further contains machinery for generating fresh behaviour identifiers. This includes an extra field fresh in the Cfg structure, as well as well-formedness rules ensuring freshness of fresh. Similarly, there is an assumption that there is always a larger timestamp available.

Additionally, there is a definition of a complete execution (Model.complete), where no more events are possible and a corresponding definition for histories (History.complete). There is a proof that a complete history matches a configuration without any running or pending behaviours (cfg_done_history_complete) as well as a proof that a complete history translates into a complete execution (model_from_history_complete). Finally, there is an example of a starting configuration with a well-formed and matching history, showing that there is some configuration from which the preservation theorem can be applied (starting_cfg_wf).