Bring formalisation closer to the paper
A number of changes is proposed with the purpose of bringing the formalisation closer to the presentation found in the paper. These modifications are mainly four:
-
The fancy update modalities are removed from the definition of
protocol_agreement
. -
The protocol subsumption
iEff_le
is redefined in terms of the more abstract notion ofprotocol_agreement
. -
The later modalities in the definitions of both
shallow_handler
anddeep_handler
are replaced to give rise to correctness judgements that are easier to prove. -
The verification of the scheduler is revised.