Thm* E:EventStruct, P:TraceProperty(E), A:Type, evt:(A![](FONT/dash.png) |E|)
, tg:(A![](FONT/dash.png) Label), tr_u:Trace(E), tr_l:A List.
switchable(E)(P) ![](FONT/eq.png)
No-dup-send(E)(tr_u) ![](FONT/eq.png)
full_switch_inv(E;A;evt;tg;tr_u;tr_l) ![](FONT/eq.png) ( m:Label. P(map(evt; < tr_l > _m))) ![](FONT/eq.png) P(tr_u) | [switch_main_theorem] |
Thm* E:EventStruct, P:((|E| List)![](FONT/dash.png) Prop), A:Type, evt:(A![](FONT/dash.png) |E|), tg:(A![](FONT/dash.png) Label)
, tr:A List.
switchable(E)(P) ![](FONT/eq.png)
No-dup-send(E)(map(evt;tr)) ![](FONT/eq.png)
switch_inv( < A,evt,tg > (E))(tr) ![](FONT/eq.png) ( m:Label. P(map(evt; < tr > _m))) ![](FONT/eq.png) P(map(evt;tr)) | [switch_theorem] |
Thm* E:TaggedEventStruct, P:TraceProperty(E).
switchable(E)(P) ![](FONT/eq.png) ((switch_inv(E) No-dup-send(E)) fuses P) | [switch_inv_theorem2] |
Thm* E:TaggedEventStruct, P:TraceProperty(E).
MCS(E)(P) ![](FONT/eq.png)
asyncR(E) preserves P ![](FONT/eq.png)
delayableR(E) preserves P ![](FONT/eq.png)
(P refines (Causal(E) No-dup-deliver(E))) ![](FONT/eq.png) ((switch_inv(E) No-dup-send(E)) fuses P) | [switch_inv_theorem] |
Thm* E:TaggedEventStruct, P:TraceProperty(E).
MCS(E)(P) ![](FONT/eq.png)
(P refines (Causal(E) No-dup-deliver(E))) ![](FONT/eq.png)
(((switch_inv(E) AD-normal(E)) No-dup-send(E)) fuses P) | [switch_inv_plus_normal] |
Thm* E:EventStruct, P:((|E| List)![](FONT/dash.png) Prop), A:Type, f:(A![](FONT/dash.png) |E|)
, t:(A![](FONT/dash.png) Label). switchable(E)(P) ![](FONT/eq.png) switchable( < A,f,t > (E))(P o f) | [switchable_induced_tagged] |
Thm* E:TaggedEventStruct, tr:Trace(E).
(switch_inv(E) No-dup-send(E))(tr) ![](FONT/eq.png)
( tr':Trace(E). switch_inv(E)(tr') & AD-normal(E)(tr') & (tr adR(E) tr')) | [switch_normal_exists] |
Thm* E:TaggedEventStruct.
(switch_inv(E) Causal(E) AD-normal(E) No-dup-deliver(E)) refines switch-decomposable(E) | [strong_switch_inv_decomposable] |
Thm* E:EventStruct.
switchable(E)(totalorder(E) Causal(E) No-dup-deliver(E)) | [totalorder_switchable] |
Thm* E:EventStruct, A:Type, f:(A![](FONT/dash.png) |E|), P:((|E| List)![](FONT/dash.png) Prop).
switchable(E)(P) ![](FONT/eq.png) switchable(induced_event_str(E;A;f))(P o f) | [switchable_induced] |
Thm* E:TaggedEventStruct. tag_splitable(E;adR(E)) | [tag_sublist_layer] |
Thm* E:EventStruct, tr:|E| List, ls: ||tr||.
is-send(E)(tr[ls]) ![](FONT/eq.png)
( j: ||tr||. ls < j ![](FONT/eq.png) is-send(E)(tr[j])) ![](FONT/eq.png)
( i,j: ||tr||. i j ![](FONT/eq.png) is-send(E)(tr[j]) ![](FONT/eq.png) (i (switchR(tr)^*) ls) ![](FONT/eq.png) (j (switchR(tr)^*) ls)) | [switch_inv_rel_closure_lemma1] |
Thm* E:TaggedEventStruct, tr:|E| List, ls: ||tr||.
switch_inv(E)(tr) ![](FONT/eq.png)
( i,j: ||tr||. (i (switchR(tr)^*) ls) ![](FONT/eq.png) (j (switchR(tr)^*) ls) ![](FONT/eq.png) tag(E)(tr[i]) = tag(E)(tr[j])) | [switch_inv_rel_closure] |
Thm* E:EventStruct, P:TraceProperty(E).
switchable0(E)(P) ![](FONT/eq.png) switchable(E)(P Causal(E) No-dup-deliver(E)) | [switchable0_switchable] |
Thm* E:EventStruct. switchable0(E)(totalorder(E)) | [totalorder_switchable0] |
Thm* E:TaggedEventStruct, tr:|E| List.
switch_inv(E)(tr) ![](FONT/if_big.png) ( i,j: ||tr||. (i switchR(tr) j) ![](FONT/eq.png) tag(E)(tr[i]) = tag(E)(tr[j])) | [switch_inv_rel_same_tag] |
Thm* E:EventStruct, tr:|E| List, ls,i: ||tr||.
is-send(E)(tr[ls]) ![](FONT/eq.png) (i (switchR(tr)^*) ls) ![](FONT/eq.png) is-send(E)(tr[i]) | [switch_inv_rel_closure_send] |
Thm* E:EventStruct. switchable0(E)(No-dup-deliver(E)) | [P_no_dup_switchable0] |
Thm* E:EventStruct. switchable0(E)(Causal(E)) | [P_causal_switchable0] |
Thm* E:EventStruct, P:((Label![](FONT/dash.png) (|E| List))![](FONT/dash.png) Prop).
( f,g:(Label![](FONT/dash.png) (|E| List)). ( p:Label. g(p) f(p)) ![](FONT/eq.png) P(f) ![](FONT/eq.png) P(g)) ![](FONT/eq.png)
( f,g:(Label![](FONT/dash.png) (|E| List)).
( a:|E|. p:Label. g(p) = filter( b.![](FONT/not.png) (b =msg=(E) a);f(p))) ![](FONT/eq.png) P(f) ![](FONT/eq.png) P(g))
![](FONT/eq.png)
( f,g,h:(Label![](FONT/dash.png) (|E| List)).
( p,q:Label. ( x f(p).( y g(q). (x =msg=(E) y)))) ![](FONT/eq.png)
( p:Label. h(p) = ((f(p)) @ (g(p)))) ![](FONT/eq.png) P(f) ![](FONT/eq.png) P(g) ![](FONT/eq.png) P(h))
![](FONT/eq.png)
switchable0(E)(local_deliver_property(E;P)) | [local_deliver_switchable] |
Thm* E:EventStruct, x:|E| List, j,z: ||x||. Dec(j switchR(x) z) | [decidable__switch_inv_rel] |
Thm* E:EventStruct. layerR(E)^-1 preserves No-dup-send(E) | [no_duplicate_send_layer] |
Thm* E:TaggedEventStruct. safetyR(E) preserves switch_inv(E) | [switch_inv_safety] |
Thm* E:TaggedEventStruct, x:|E| List, i: (||x||-1).
switch_inv(E)(x) ![](FONT/eq.png)
is-send(E)(x[(i+1)]) ![](FONT/eq.png)
is-send(E)(x[i]) loc(E)(x[i]) = loc(E)(x[(i+1)]) ![](FONT/eq.png) switch_inv(E)(swap(x;i;i+1)) | [switch_inv_swap] |
Thm* E:TaggedEventStruct. switch_inv(E) (|E| List)![](FONT/dash.png) Prop | [switch_inv_wf] |
Thm* E:EventStruct, x,y:|E| List. (x asyncR(E) y) ![](FONT/eq.png) (y asyncR(E) x) | [R_async_symmetric] |
Thm* E:EventStruct, P:TraceProperty(E).
R_permutation(E) preserves P ![](FONT/eq.png) asyncR(E) preserves P | [permutable_implies_async] |
Thm* E:EventStruct. asyncR(E) preserves No-dup-send(E) | [no_duplicate_send_async] |
Thm* E:EventStruct, x,y:|E| List.
(x delayableR(E) y) ![](FONT/eq.png) (y delayableR(E) x) | [R_delayable_symmetric] |
Thm* E:EventStruct, P:TraceProperty(E).
R_permutation(E) preserves P ![](FONT/eq.png) delayableR(E) preserves P | [permutable_implies_delayable] |
Thm* E:EventStruct. delayableR(E) preserves No-dup-send(E) | [no_duplicate_send_delayable] |
Thm* E:EventStruct. R_permutation(E) preserves No-dup-deliver(E) | [P_no_dup_permutable] |
Thm* E:TaggedEventStruct, P,I:TraceProperty(E).
MCS(E)(P) ![](FONT/eq.png) safetyR(E) preserves I ![](FONT/eq.png) (I refines single-tag-decomposable(E)) ![](FONT/eq.png) (I fuses P) | [M_DASH_C_DASH_S_SPACE_induction] |
Thm* E:EventStruct, a,b,c:|E|, tr:|E| List.
a somewhere delivered before b ![](FONT/eq.png) a somewhere delivered before c c somewhere delivered before b | [delivered_before_somewhere_lemma] |
Thm* E:TaggedEventStruct. safetyR(E) preserves AD-normal(E) | [switch_normal_safety] |
Thm* E:TaggedEventStruct.
(switch-decomposable(E) Tag-by-msg(E) Causal(E) No-dup-send(E))
refines single-tag-decomposable(E) | [switch_decomp_implies_single_tag_decomp] |
Thm* E:EventStruct, a,b:|E|, tr:|E| List.
a somewhere delivered before b
![](FONT/if_big.png)
( k: ||tr||.
a delivered at time k ![](FONT/eq.png)
( k': ||tr||. k' < k & b delivered at time k' & loc(E)(tr[k']) = loc(E)(tr[k]))) | [not_delivered_before_somewhere] |
Thm* E:EventStruct, tr:|E| List, x,y:|E|.
Dec(x somewhere delivered before y) | [decidable__delivered_before_somewhere] |
Thm* E:EventStruct, A:Type, evt:(A![](FONT/dash.png) |E|), tg:(A![](FONT/dash.png) Label), m:Label
, tr1,tr2:A List. (tr1 R(tg) tr2) ![](FONT/eq.png) < tr1 > _m = < tr2 > _m A List | [tag_sublist_preserved] |
Thm* E:EventStruct. totalorder(E) TraceProperty(E) | [totalorder_wf] |
Thm* E:TaggedEventStruct, P,I:((|E| List)![](FONT/dash.png) Prop).
(P refines (Causal(E) No-dup-deliver(E))) ![](FONT/eq.png)
((I No-dup-send(E) Tag-by-msg(E) Causal(E) No-dup-deliver(E)) fuses P) ![](FONT/eq.png)
((I No-dup-send(E)) fuses P) | [no_DASH_dup_DASH_fusion] |
Thm* E:TaggedEventStruct. Tag-by-msg(E) fuses No-dup-deliver(E) | [no_dup_fusion] |
Thm* E:TaggedEventStruct, P,I:((|E| List)![](FONT/dash.png) Prop).
(P refines Causal(E)) ![](FONT/eq.png)
((I No-dup-send(E) Tag-by-msg(E)) fuses P) ![](FONT/eq.png) ((I No-dup-send(E)) fuses P) | [tag_by_msg_fusion_lemma] |
Thm* E:TaggedEventStruct. safetyR(E) preserves Tag-by-msg(E) | [P_tag_by_msg_safety] |
Thm* E:EventStruct. safetyR(E) preserves No-dup-deliver(E) | [P_no_dup_deliver_safety] |
Thm* E:TaggedEventStruct, P,I,J,K:TraceProperty(E)
, R:(Trace(E)![](FONT/dash.png) Trace(E)![](FONT/dash.png) Prop).
tag_splitable(E;R) ![](FONT/eq.png)
( tr_1,tr_2:Trace(E). (tr_1 R tr_2) ![](FONT/eq.png) (tr_2 R tr_1)) ![](FONT/eq.png)
R preserves P ![](FONT/eq.png)
R preserves K ![](FONT/eq.png)
( tr:Trace(E). (I K)(tr) ![](FONT/eq.png) ( tr':Trace(E). I(tr') & J(tr') & (tr R tr'))) ![](FONT/eq.png)
(((I J) K) fuses P) ![](FONT/eq.png) ((I K) fuses P) | [normal_form_fusion] |
Thm* E:EventStruct, P:TraceProperty(E), L,L1:|E| List.
memorylessR(E) preserves P ![](FONT/eq.png) P(L) ![](FONT/eq.png) P((L -x =msg=(E) y L1)) | [memoryless_remove_msgs] |
Thm* E:TaggedEventStruct, I,J,P:TraceProperty(E).
((I J) fuses P) ![](FONT/eq.png) (I fuses J) ![](FONT/eq.png) (P refines J) ![](FONT/eq.png) (I fuses P) | [fusion_simplification] |
Thm* E:EventStruct, P:TraceProperty(E).
R_strong_safety(E) preserves P ![](FONT/eq.png) memorylessR(E) preserves P | [strong_safety_implies_memoryless] |
Thm* E:EventStruct, P:TraceProperty(E).
R_strong_safety(E) preserves P ![](FONT/eq.png) safetyR(E) preserves P | [strong_safety_implies_safety] |
Thm* E:TaggedEventStruct, I,P,Q:TraceProperty(E).
(I fuses P) ![](FONT/eq.png) (I fuses Q) ![](FONT/eq.png) (I fuses (P Q)) | [fusion_and] |
Thm* E:TaggedEventStruct, I,J,P:TraceProperty(E).
(J refines I) ![](FONT/eq.png) (I fuses P) ![](FONT/eq.png) (J fuses P) | [fusion_weakening] |
Thm* E:Structure, P,Q_1,Q_2:((|E| List)![](FONT/dash.png) Prop).
(P refines Q_1) ![](FONT/eq.png) (P refines Q_2) ![](FONT/eq.png) (P refines (Q_1 Q_2)) | [tr_refines_and] |
Thm* E:EventStruct. send-enabledR(E) preserves No-dup-deliver(E) | [P_no_dup_send_enabled] |
Thm* E:EventStruct. safetyR(E) preserves Causal(E) | [P_causal_safety] |
Thm* E:EventStruct. safetyR(E) preserves No-dup-send(E) | [no_duplicate_send_safety] |
Thm* E:EventStruct. R_strong_safety(E) preserves No-dup-deliver(E) | [P_no_dup_strong_safety] |
Thm* E:EventStruct. (ternary) composableR(E) preserves No-dup-deliver(E) | [P_no_dup_composable] |
Thm* E:TaggedEventStruct, tr:|E| List, x,y:|E|.
Dec(R_ad_normal(tr)(x,y)) | [decidable__R_ad_normal] |
Thm* E:TaggedEventStruct. PTrue fuses Causal(E) | [causal_fusion] |
Thm* E:EventStruct, L:|E| List.
L = nil ![](FONT/eq.png) Causal(E)(L) ![](FONT/eq.png) ( i: ||L||. is-send(E)(L[i])) | [P_causal_non_nil] |
Thm* E:TaggedEventStruct, tr:|E| List.
( m:Label. Causal(E)( < tr > _m)) ![](FONT/eq.png) No-dup-send(E)(tr) ![](FONT/eq.png) Tag-by-msg(E)(tr) | [P_tag_by_msg_lemma] |
Thm* E:EventStruct, tr:|E| List.
No-dup-deliver(E)(tr)
![](FONT/if_big.png)
( x,y:|E|.
is-send(E)(x) ![](FONT/eq.png)
is-send(E)(y) ![](FONT/eq.png) (y =msg=(E) x) ![](FONT/eq.png) loc(E)(x) = loc(E)(y) ![](FONT/eq.png) sublist(|E|;[x; y];tr)) | [P_no_dup_iff] |
Thm* E:EventStruct, tr:|E| List.
Causal(E)(tr) ![](FONT/if_big.png) ( tr':|E| List. tr' tr ![](FONT/eq.png) ( x tr'.( y tr'.is-send(E)(y) & (y =msg=(E) x)))) | [P_causal_iff] |
Thm* msg:(A![](FONT/dash.png) A![](FONT/dash.png) ![](FONT/then_med.png) ), L1,L2:A List.
( a,b:A. (a L1) ![](FONT/eq.png) (b L2) ![](FONT/eq.png) msg(a,b)) ![](FONT/eq.png) (L1 -msg(a,b) L2) = L1 | [remove_msgs_disjoint] |
Thm* msg:(A![](FONT/dash.png) A![](FONT/dash.png) ![](FONT/then_med.png) ), L1,L2:A List.
( x:A. (x L1) ![](FONT/eq.png) (x L2)) ![](FONT/eq.png) Refl(A)(msg(_1,_2)) ![](FONT/eq.png) (L1 -msg(a,b) L2) = nil | [remove_msgs_nil] |
Thm* E:EventStruct, A:Type, evt:(A![](FONT/dash.png) |E|), tg:(A![](FONT/dash.png) Label), tr_l:A List.
No-dup-send(E)(map(evt;tr_l)) ![](FONT/eq.png) No-dup-send( < A,evt,tg > (E))(tr_l) | [no_dup_send_induced] |
Def switch_inv(E)(tr)
== i,j,k: ||tr||.
i < j ![](FONT/eq.png)
(is-send(E)(tr[i])) ![](FONT/eq.png)
(is-send(E)(tr[j])) ![](FONT/eq.png)
tag(E)(tr[i]) = tag(E)(tr[j]) ![](FONT/eq.png)
tr[j] delivered at time k ![](FONT/eq.png)
( k': ||tr||. k' < k & tr[i] delivered at time k' & loc(E)(tr[k']) = loc(E)(tr[k])) | [switch_inv] |
Def switch-decomposable(E)(L)
== L = nil |E| List
( Q:( ||L||![](FONT/dash.png) Prop).
( i: ||L||. Dec(Q(i)))
& ( i: ||L||. Q(i))
& ( i: ||L||. Q(i) ![](FONT/eq.png) (is-send(E)(L[i])))
& ( i,j: ||L||. Q(i) ![](FONT/eq.png) Q(j) ![](FONT/eq.png) tag(E)(L[i]) = tag(E)(L[j]))
& ( i,j: ||L||. Q(i) ![](FONT/eq.png) i j ![](FONT/eq.png) C(Q)(j))) | [switch_decomposable] |
Def AD-normal(E)(tr)
== i: (||tr||-1).
( (is-send(E)(tr[i])) ![](FONT/eq.png) ![](FONT/not.png) (is-send(E)(tr[(i+1)])) ![](FONT/eq.png) (tr[i] =msg=(E) tr[(i+1)]))
& (( x,y: ||tr||.
x < y
& (is-send(E)(tr[x]))
& (is-send(E)(tr[y]))
& tr[x] delivered at time i+1
& tr[y] delivered at time i)
![](FONT/eq.png)
loc(E)(tr[i]) = loc(E)(tr[(i+1)])) | [switch_normal] |
Def x somewhere delivered before y
== k: ||tr||.
x delivered at time k
& ( k': ||tr||. y delivered at time k' ![](FONT/eq.png) loc(E)(tr[k']) = loc(E)(tr[k]) ![](FONT/eq.png) k k') | [delivered_before_somewhere] |
Def totalorder(E)(tr)
== p,q:Label. agree_on_common(|MS(E)|;map(msg(E);tr delivered at p);map(msg(E);tr delivered at q)) | [totalorder] |
Def P refines Q == tr:|E| List. P(tr) ![](FONT/eq.png) Q(tr) | [tr_refines] |
Def I fuses P == tr:Trace(E). ( m:Label. P( < tr > _m)) ![](FONT/eq.png) I(tr) ![](FONT/eq.png) P(tr) | [fusion_condition] |
Def Causal(E)(tr)
== i: ||tr||. j: ||tr||. j i & (is-send(E)(tr[j])) & (tr[j] =msg=(E) tr[i]) | [P_causal] |
Def No-dup-deliver(E)(tr)
== i,j: ||tr||.
![](FONT/not.png) (is-send(E)(tr[i])) ![](FONT/eq.png)
![](FONT/not.png) (is-send(E)(tr[j])) ![](FONT/eq.png) (tr[j] =msg=(E) tr[i]) ![](FONT/eq.png) loc(E)(tr[i]) = loc(E)(tr[j]) ![](FONT/eq.png) i = j | [P_no_dup] |
Def Tag-by-msg(E)(tr)
== i,j: ||tr||. (tr[i] =msg=(E) tr[j]) ![](FONT/eq.png) tag(E)(tr[i]) = tag(E)(tr[j]) | [P_tag_by_msg] |
Def switch_inv(E; tr)
== i,j,k: ||tr||.
i < j ![](FONT/eq.png)
(is-send(E)(tr[i])) ![](FONT/eq.png)
(is-send(E)(tr[j])) ![](FONT/eq.png)
tag(E)(tr[i]) = tag(E)(tr[j]) ![](FONT/eq.png)
(tr[j] =msg=(E) tr[k]) ![](FONT/eq.png)
![](FONT/not.png) (is-send(E)(tr[k])) ![](FONT/eq.png)
( k': ||tr||.
k' < k & loc(E)(tr[k']) = loc(E)(tr[k]) & (tr[i] =msg=(E) tr[k']) & ![](FONT/not.png) (is-send(E)(tr[k']))) | [switch_inv2001_03_15_DASH_PM_DASH_12_53_21] |