-
Notifications
You must be signed in to change notification settings - Fork 83
/
MessagesAndRefinement.v
1471 lines (1266 loc) · 44.5 KB
/
MessagesAndRefinement.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
(** Formal Reasoning About Programs <http://adam.chlipala.net/frap/>
* Chapter 21: Process Algebra and Behavioral Refinement
* Author: Adam Chlipala
* License: https://creativecommons.org/licenses/by-nc-nd/4.0/ *)
Require Import Frap Eqdep FunctionalExtensionality.
Set Implicit Arguments.
Set Asymmetric Patterns.
(** * First, an unexplained tactic that will come in handy.... *)
Ltac invert H := (FrapWithoutSets.invert H || (inversion H; clear H));
repeat match goal with
| [ x : _ |- _ ] => subst x
| [ H : existT _ _ _ = existT _ _ _ |- _ ] => apply inj_pair2 in H; try subst
end.
(** * A process algebra: syntax and semantics *)
(* A process algebra defines a set of communicating *processes*, which might
* more commonly be called *threads*. Typically processes communicate not with
* locks and shared memory, as they have in the prior two chapters, but instead
* with *message passing*. Messages are passed over synchronous *channels*,
* which we will just represent as numbers. *)
Notation channel := nat (only parsing).
(* Here are the basic syntactic constructions of processes. *)
Inductive proc :=
| NewChannel (notThese : list channel) (k : channel -> proc)
(* Pick a new channel name [ch] not found in [notThese] and continue like
* [k ch]. *)
| BlockChannel (ch : channel) (pr : proc)
(* Act like [pr] but prevent interaction with other processes through channel
* [ch]. We effectively force [ch] to be *private*. *)
| Send (ch : channel) {A : Type} (v : A) (k : proc)
| Recv (ch : channel) {A : Type} (k : A -> proc)
(* When one process runs a [Send] and the other a [Recv] on the same channel
* simultaneously, the [Send] moves on to its [k], while the [Recv] moves on to
* its [k v], for [v] the value that was sent. *)
| Par (pr1 pr2 : proc)
(* This one, at least, is just like it was in the last chapter: parallel
* composition of threads. *)
| Dup (pr : proc)
(* An idiosyncratic convention of process algebra: [Dup pr] acts like an
* *infinite* number of *copies* of [pr]. It replaces conventional loops. *)
| Done
(* This process can't do anything *).
(* Some nicer notations: *)
Notation "'New' ls ( x ) ; k" := (NewChannel ls (fun x => k)) (right associativity, at level 51, ls at level 0).
Notation "'Block' ch ; k" := (BlockChannel ch k) (right associativity, at level 51).
Notation "!! ch ( v ) ; k" := (Send ch v k) (right associativity, at level 45, ch at level 0).
Notation "?? ch ( x : T ) ; k" := (Recv ch (fun x : T => k)) (right associativity, at level 45, ch at level 0, x at level 0).
Infix "||" := Par.
(** * Example *)
(* Let's build highly exciting processes for adding constants to numbers. *)
(* This one accepts one number [n] on channel [input] and returns [n + k] as the
* result, by writing it to [output]. *)
Definition addN (k : nat) (input output : channel) : proc :=
??input(n : nat);
!!output(n + k);
Done.
(* We wrap that last one in a [Dup] to turn it into a kind of immortal server,
* happy to keep responding to "please add k to this" requests forever. *)
Definition addNs (k : nat) (input output : channel) : proc :=
Dup (addN k input output).
(* Chaining together two "+1" boxes is one way to build an alternative "+2"
* box! *)
Definition add2 (input output : channel) : proc :=
Dup (New[input;output](intermediate);
addN 1 input intermediate
|| addN 1 intermediate output).
(* However we implement addition, we might compose with this tester process,
* which uses an adder as a subroutine in a larger protocol. [metaInput] and
* [metaOutput] are the input and output of the whole system, while [input] and
* [output] are used internally, say to communicate with an adder. *)
Definition tester (metaInput input output metaOutput : channel) : proc :=
??metaInput(n : nat);
!!input(n * 2);
??output(r : nat);
!!metaOutput(r);
Done.
(** * Labeled semantics *)
(* Let's explain how programs run. We'll give a flavor of operational semantics
* called a "labeled transition system," because each step will include a label
* that explains what happened. In this case, the only relevant happenings are
* sends or receives on channels. Crucially, we suppress send/receive labels
* for operations blocked by [Block]s. *)
Record message := {
Channel : channel;
TypeOf : Type;
Value : TypeOf
}.
Inductive action :=
| Output (m : message)
| Input (m : message).
Inductive label :=
| Silent
| Action (a : action).
(* This predicate captures when a label doesn't use a channel. *)
Definition notUse (ch : channel) (l : label) :=
match l with
| Action (Input r) => r.(Channel) <> ch
| Action (Output r) => r.(Channel) <> ch
| Silent => True
end.
(* Now, our labeled transition system: *)
Inductive lstep : proc -> label -> proc -> Prop :=
(* Sends and receives generate the expected labels. Note that, for a [Recv],
* the value being received is "pulled out of thin air"! However, it gets
* determined concretely by comparing against a matching [Send], in a rule that
* we get to shortly. *)
| LStepSend : forall ch {A : Type} (v : A) k,
lstep (Send ch v k)
(Action (Output {| Channel := ch; Value := v |}))
k
| LStepRecv : forall ch {A : Type} (k : A -> _) v,
lstep (Recv ch k)
(Action (Input {| Channel := ch; Value := v |}))
(k v)
(* A [Dup] always has the option of replicating itself further. *)
| LStepDup : forall pr,
lstep (Dup pr) Silent (Par (Dup pr) pr)
(* A channel-allocation operation nondeterministically picks the new channel ID,
* only checking that it isn't in the provided blacklist. We install a [Block]
* node to keep this channel truly private. *)
| LStepNew : forall chs ch k,
~In ch chs
-> lstep (NewChannel chs k) Silent (BlockChannel ch (k ch))
(* [Block] nodes work as expected, disallowing labels that use the channel. *)
| LStepBlock : forall ch k l k',
lstep k l k'
-> notUse ch l
-> lstep (BlockChannel ch k) l (BlockChannel ch k')
(* When either side of a parallel composition can step, we may bubble that step
* up to the top. *)
| LStepPar1 : forall pr1 pr2 l pr1',
lstep pr1 l pr1'
-> lstep (Par pr1 pr2) l (Par pr1' pr2)
| LStepPar2 : forall pr1 pr2 l pr2',
lstep pr2 l pr2'
-> lstep (Par pr1 pr2) l (Par pr1 pr2')
(* These two symmetrical rules are the heart of how communication happens in our
* language. Namely, in a parallel composition, when one side is prepared to
* write a value to a channel, and the other side is prepared to read the same
* value from the same channel, the two sides *rendezvous*, and the value is
* exchanged. This is the only mechanism to let two transitions happen at
* once. *)
| LStepRendezvousLeft : forall pr1 ch {A : Type} (v : A) pr1' pr2 pr2',
lstep pr1 (Action (Input {| Channel := ch; Value := v |})) pr1'
-> lstep pr2 (Action (Output {| Channel := ch; Value := v |})) pr2'
-> lstep (Par pr1 pr2) Silent (Par pr1' pr2')
| LStepRendezvousRight : forall pr1 ch {A : Type} (v : A) pr1' pr2 pr2',
lstep pr1 (Action (Output {| Channel := ch; Value := v |})) pr1'
-> lstep pr2 (Action (Input {| Channel := ch; Value := v |})) pr2'
-> lstep (Par pr1 pr2) Silent (Par pr1' pr2').
(* Here's a shorthand for silent steps. *)
Definition lstepSilent (pr1 pr2 : proc) := lstep pr1 Silent pr2.
(* Our key proof task will be to prove that one process "acts like" another.
* We'll use *simulation* as the precise notion of "acts like." *)
(* We say that a relation [R] is a *simulation* when it satisfies the first two
* conditions below. The [simulates] predicate additionally asserts that a
* particular pair of processes belongs to [R]. *)
Definition simulates (R : proc -> proc -> Prop) (pr1 pr2 : proc) :=
(* First, consider a pair of processes related by [R]. When the lefthand
* process can take a silent step, the righthand process can take zero or more
* silent steps to "catch up," arriving at a new righthand process related to
* the new lefthand process. *)
(forall pr1 pr2, R pr1 pr2
-> forall pr1', lstepSilent pr1 pr1'
-> exists pr2', lstepSilent^* pr2 pr2'
/\ R pr1' pr2')
(* Now consider the same scenario where the lefthand process takes a nonsilent
* step. We require that the righthand process can "catch up" in a way that
* generates the same label that the lefthand process generated. *)
/\ (forall pr1 pr2, R pr1 pr2
-> forall a pr1', lstep pr1 (Action a) pr1'
-> exists pr2' pr2'', lstepSilent^* pr2 pr2'
/\ lstep pr2' (Action a) pr2''
/\ R pr1' pr2'')
(* Finally, the provided process pair is in the relation. *)
/\ R pr1 pr2.
(* One process *refines* another when there exists some simulation. *)
Definition refines (pr1 pr2 : proc) :=
exists R, simulates R pr1 pr2.
Infix "<|" := refines (no associativity, at level 70).
(* That's a somewhat fancy notion of compatibility! We can also relate it to
* more intuitive conditions that aren't strong enough for many of the proofs we
* want to do later. *)
(* This predicate captures all finite traces of actions that a process could
* generate. *)
Inductive couldGenerate : proc -> list action -> Prop :=
| CgNothing : forall pr,
couldGenerate pr []
| CgSilent : forall pr pr' tr,
lstep pr Silent pr'
-> couldGenerate pr' tr
-> couldGenerate pr tr
| CgAction : forall pr a pr' tr,
lstep pr (Action a) pr'
-> couldGenerate pr' tr
-> couldGenerate pr (a :: tr).
(* Skip ahead to [refines_couldGenerate] to see the top-level connection from
* [refines]. *)
Global Hint Constructors couldGenerate : core.
Lemma lstepSilent_couldGenerate : forall pr1 pr2,
lstepSilent^* pr1 pr2
-> forall tr, couldGenerate pr2 tr
-> couldGenerate pr1 tr.
Proof.
induct 1; eauto.
Qed.
Global Hint Resolve lstepSilent_couldGenerate : core.
Lemma simulates_couldGenerate' : forall (R : proc -> proc -> Prop),
(forall pr1 pr2, R pr1 pr2
-> forall pr1', lstepSilent pr1 pr1'
-> exists pr2', lstepSilent^* pr2 pr2'
/\ R pr1' pr2')
-> (forall pr1 pr2, R pr1 pr2
-> forall a pr1', lstep pr1 (Action a) pr1'
-> exists pr2' pr2'', lstepSilent^* pr2 pr2'
/\ lstep pr2' (Action a) pr2''
/\ R pr1' pr2'')
-> forall pr1 tr, couldGenerate pr1 tr
-> forall pr2, R pr1 pr2
-> couldGenerate pr2 tr.
Proof.
induct 3; simplify; auto.
eapply H in H1; eauto.
first_order.
eauto.
eapply H0 in H1; eauto.
first_order.
eauto.
Qed.
(* This theorem says that refinement implies *trace inclusion*. *)
Theorem refines_couldGenerate : forall pr1 pr2, pr1 <| pr2
-> forall tr, couldGenerate pr1 tr
-> couldGenerate pr2 tr.
Proof.
unfold refines; first_order; eauto using simulates_couldGenerate'.
Qed.
(** * Tactics for automating refinement proofs *)
(* Well, you're used to unexplained automation tactics by now, so here are some
* more. ;-) *)
Lemma invert_Recv : forall ch (A : Type) (k : A -> proc) (x : A) pr,
lstep (Recv ch k) (Action (Input {| Channel := ch; Value := x |})) pr
-> pr = k x.
Proof.
invert 1; auto.
Qed.
Ltac inverter :=
repeat match goal with
| [ H : lstep _ _ _ |- _ ] => (apply invert_Recv in H; try subst) || invert H
| [ H : lstepSilent _ _ |- _ ] => invert H
end.
Global Hint Constructors lstep : core.
Global Hint Unfold lstepSilent : core.
Ltac lists' :=
repeat match goal with
| [ H : NoDup _ |- _ ] => invert H
| [ |- NoDup _ ] => constructor
end; simplify; propositional; equality || linear_arithmetic.
Ltac lists := solve [ lists' ].
Global Hint Extern 1 (NoDup _) => lists : core.
(** * Examples *)
(* OK, let's verify a simplification of the example we started with. *)
Definition add2_once (input output : channel) : proc :=
New[input;output](intermediate);
(addN 1 input intermediate
|| addN 1 intermediate output).
(* Here's our first, painstakingly crafted simulation relation. It needs to
* identify all pairs of processes that should be considered compatible. Think
* of the first process as the fancy *implementation* and the second process as
* the simpler *specification*. *)
Inductive R_add2 : proc -> proc -> Prop :=
| Starting : forall input output,
input <> output
-> R_add2
(New[input;output](ch); ??input(n : nat); !!ch(n + 1); Done
|| ??ch(n : nat); !!output (n + 1); Done)
(??input(n : nat); !!output(n + 2); Done)
| ChoseIntermediate : forall input output intermediate,
NoDup [input; output; intermediate]
-> R_add2
(Block intermediate; ??input(n : nat); !!intermediate(n + 1); Done
|| ??intermediate(n : nat); !!output (n + 1); Done)
(??input(n : nat); !!output(n + 2); Done)
| GotInput : forall input output intermediate n,
NoDup [input; output; intermediate]
-> R_add2
(Block intermediate; !!intermediate(n + 1); Done
|| ??intermediate(n : nat); !!output (n + 1); Done)
(!!output(n + 2); Done)
| HandedOff : forall input output intermediate n,
NoDup [input; output; intermediate]
-> R_add2
(Block intermediate; Done || (!!output(n + 2); Done))
(!!output(n + 2); Done)
| Finished : forall input output intermediate,
NoDup [input; output; intermediate]
-> R_add2
(Block intermediate; Done || Done)
Done.
Global Hint Constructors R_add2 : core.
Theorem add2_once_refines_addN : forall input output,
input <> output
-> add2_once input output <| addN 2 input output.
Proof.
simplify.
exists R_add2.
first_order.
invert H0; simplify; inverter; eauto.
replace (n + 1 + 1) with (n + 2) by linear_arithmetic.
eauto.
invert H0; simplify; inverter; eauto 10; simplify; equality.
unfold add2_once, addN; eauto.
Qed.
(* Well, good! The fancy version doesn't produce any traces that the simple
* version couldn't also produce. (It may, however, fail to produce some traces
* that the spec allows.) *)
(** * Compositional reasoning principles *)
(* It turns out that refinement has all sorts of convenient algebraic
* properties. To start with, it's a preorder. *)
Theorem refines_refl : forall pr,
pr <| pr.
Proof.
simplify.
exists (fun pr1 pr2 => pr1 = pr2).
first_order; subst; eauto.
Qed.
Lemma refines_trans' : forall R : _ -> _ -> Prop,
(forall pr1 pr2,
R pr1 pr2
-> forall pr1', lstepSilent pr1 pr1'
-> exists pr2', lstepSilent^* pr2 pr2' /\ R pr1' pr2')
-> forall pr1 pr1', lstepSilent^* pr1 pr1'
-> forall pr2, R pr1 pr2
-> exists pr2', R pr1' pr2' /\ lstepSilent^* pr2 pr2'.
Proof.
induct 2; simplify; eauto.
eapply H in H0; eauto.
first_order.
apply IHtrc in H3.
first_order.
eauto using trc_trans.
Qed.
Theorem refines_trans : forall pr1 pr2 pr3,
pr1 <| pr2
-> pr2 <| pr3
-> pr1 <| pr3.
Proof.
invert 1; invert 1.
exists (fun p q => exists r, x p r /\ x0 r q).
first_order.
match goal with
| [ H : _, H' : x _ _ |- _ ] => eapply H in H'; eauto; []
end.
first_order.
eapply refines_trans' with (R := x0) in H7; eauto.
first_order.
match goal with
| [ H : _, H' : x _ _ |- _ ] => eapply H in H'; eauto; []
end.
first_order.
eapply refines_trans' with (R := x0) in H7; eauto.
first_order.
match goal with
| [ H : _, H' : x0 _ _ |- _ ] => eapply H in H'; eauto; []
end.
first_order.
eauto 8 using trc_trans.
Qed.
(** ** Dup *)
(* Refinement can be "pushed inside" a [Dup] operation. *)
Inductive RDup (R : proc -> proc -> Prop) : proc -> proc -> Prop :=
| RDupLeaf : forall pr1 pr2,
R pr1 pr2
-> RDup R pr1 pr2
| RDupDup : forall pr1 pr2,
RDup R pr1 pr2
-> RDup R (Dup pr1) (Dup pr2)
| RDupPar : forall pr1 pr2 pr1' pr2',
RDup R pr1 pr1'
-> RDup R pr2 pr2'
-> RDup R (Par pr1 pr2) (Par pr1' pr2').
Global Hint Constructors RDup : core.
Global Hint Unfold lstepSilent : core.
Lemma lstepSilent_Par1 : forall pr1 pr1' pr2,
lstepSilent^* pr1 pr1'
-> lstepSilent^* (Par pr1 pr2) (Par pr1' pr2).
Proof.
induct 1; eauto.
Qed.
Lemma lstepSilent_Par2 : forall pr2 pr2' pr1,
lstepSilent^* pr2 pr2'
-> lstepSilent^* (Par pr1 pr2) (Par pr1 pr2').
Proof.
induct 1; eauto.
Qed.
Global Hint Resolve lstepSilent_Par1 lstepSilent_Par2 : core.
Lemma refines_Dup_Action : forall R : _ -> _ -> Prop,
(forall pr1 pr2, R pr1 pr2
-> forall pr1' a, lstep pr1 (Action a) pr1'
-> exists pr2' pr2'', lstepSilent^* pr2 pr2'
/\ lstep pr2' (Action a) pr2''
/\ R pr1' pr2'')
-> forall pr1 pr2, RDup R pr1 pr2
-> forall pr1' a, lstep pr1 (Action a) pr1'
-> exists pr2' pr2'', lstepSilent^* pr2 pr2'
/\ lstep pr2' (Action a) pr2''
/\ RDup R pr1' pr2''.
Proof.
induct 2; simplify.
eapply H in H1; eauto.
first_order.
eauto 6.
invert H1.
invert H0.
apply IHRDup1 in H5.
first_order.
eauto 10.
apply IHRDup2 in H5.
first_order.
eauto 10.
Qed.
Lemma refines_Dup_Silent : forall R : _ -> _ -> Prop,
(forall pr1 pr2, R pr1 pr2
-> forall pr1', lstepSilent pr1 pr1'
-> exists pr2', lstepSilent^* pr2 pr2'
/\ R pr1' pr2')
-> (forall pr1 pr2, R pr1 pr2
-> forall pr1' a, lstep pr1 (Action a) pr1'
-> exists pr2' pr2'', lstepSilent^* pr2 pr2'
/\ lstep pr2' (Action a) pr2''
/\ R pr1' pr2'')
-> forall pr1 pr2, RDup R pr1 pr2
-> forall pr1', lstepSilent pr1 pr1'
-> exists pr2', lstepSilent^* pr2 pr2' /\ RDup R pr1' pr2'.
Proof.
induct 3; simplify.
eapply H in H1; eauto.
first_order.
eauto.
invert H2.
eauto 10.
invert H1.
apply IHRDup1 in H6.
first_order.
eauto.
apply IHRDup2 in H6.
first_order.
eauto.
eapply refines_Dup_Action in H4; eauto.
eapply refines_Dup_Action in H5; eauto.
first_order.
eexists; propositional.
match goal with
| [ _ : lstepSilent^* pr1' ?x |- _ ] => apply trc_trans with (x || pr2')
end.
eauto.
match goal with
| [ _ : lstepSilent^* pr2' ?x' |- lstepSilent^* (?x || _) _ ] => eapply trc_trans with (x || x')
end.
eauto.
apply trc_one.
eauto.
eauto.
eapply refines_Dup_Action in H4; eauto.
eapply refines_Dup_Action in H5; eauto.
first_order.
eexists; propositional.
match goal with
| [ _ : lstepSilent^* pr1' ?x |- _ ] => apply trc_trans with (x || pr2')
end.
eauto.
match goal with
| [ _ : lstepSilent^* pr2' ?x' |- lstepSilent^* (?x || _) _ ] => eapply trc_trans with (x || x')
end.
eauto.
apply trc_one.
eauto.
eauto.
Qed.
Theorem refines_Dup : forall pr1 pr2,
pr1 <| pr2
-> Dup pr1 <| Dup pr2.
Proof.
invert 1.
exists (RDup x).
unfold simulates in *.
propositional; eauto using refines_Dup_Silent, refines_Dup_Action.
Qed.
(** ** Par *)
(* Refinement can also be "pushed inside" parallel composition. *)
Inductive RPar (R1 R2 : proc -> proc -> Prop) : proc -> proc -> Prop :=
| RPar1 : forall pr1 pr2 pr1' pr2',
R1 pr1 pr1'
-> R2 pr2 pr2'
-> RPar R1 R2 (pr1 || pr2) (pr1' || pr2').
Global Hint Constructors RPar : core.
Lemma refines_Par_Action : forall R1 R2 : _ -> _ -> Prop,
(forall pr1 pr2, R1 pr1 pr2
-> forall pr1' a, lstep pr1 (Action a) pr1'
-> exists pr2' pr2'', lstepSilent^* pr2 pr2'
/\ lstep pr2' (Action a) pr2''
/\ R1 pr1' pr2'')
-> (forall pr1 pr2, R2 pr1 pr2
-> forall pr1' a, lstep pr1 (Action a) pr1'
-> exists pr2' pr2'', lstepSilent^* pr2 pr2'
/\ lstep pr2' (Action a) pr2''
/\ R2 pr1' pr2'')
-> forall pr1 pr2, RPar R1 R2 pr1 pr2
-> forall pr1' a, lstep pr1 (Action a) pr1'
-> exists pr2' pr2'', lstepSilent^* pr2 pr2'
/\ lstep pr2' (Action a) pr2''
/\ RPar R1 R2 pr1' pr2''.
Proof.
invert 3; simplify.
invert H1.
eapply H in H8; eauto.
first_order.
eauto 10.
eapply H0 in H8; eauto.
first_order.
eauto 10.
Qed.
Lemma refines_Par_Silent : forall R1 R2 : _ -> _ -> Prop,
(forall pr1 pr2, R1 pr1 pr2
-> forall pr1', lstepSilent pr1 pr1'
-> exists pr2', lstepSilent^* pr2 pr2'
/\ R1 pr1' pr2')
-> (forall pr1 pr2, R1 pr1 pr2
-> forall pr1' a, lstep pr1 (Action a) pr1'
-> exists pr2' pr2'', lstepSilent^* pr2 pr2'
/\ lstep pr2' (Action a) pr2''
/\ R1 pr1' pr2'')
-> (forall pr1 pr2, R2 pr1 pr2
-> forall pr1', lstepSilent pr1 pr1'
-> exists pr2', lstepSilent^* pr2 pr2'
/\ R2 pr1' pr2')
-> (forall pr1 pr2, R2 pr1 pr2
-> forall pr1' a, lstep pr1 (Action a) pr1'
-> exists pr2' pr2'', lstepSilent^* pr2 pr2'
/\ lstep pr2' (Action a) pr2''
/\ R2 pr1' pr2'')
-> forall pr1 pr2, RPar R1 R2 pr1 pr2
-> forall pr1', lstepSilent pr1 pr1'
-> exists pr2', lstepSilent^* pr2 pr2' /\ RPar R1 R2 pr1' pr2'.
Proof.
invert 5; simplify.
invert H3.
eapply H in H10; eauto.
first_order; eauto.
eapply H1 in H10; eauto.
first_order; eauto.
eapply H0 in H8; eauto.
eapply H2 in H9; eauto.
first_order.
eexists; propositional.
match goal with
| [ _ : lstepSilent^* pr1' ?x |- _ ] => apply trc_trans with (x || pr2')
end.
eauto.
match goal with
| [ _ : lstepSilent^* pr2' ?x' |- lstepSilent^* (?x || _) _ ] => eapply trc_trans with (x || x')
end.
eauto.
apply trc_one.
eauto.
eauto.
eapply H0 in H8; eauto.
eapply H2 in H9; eauto.
first_order.
eexists; propositional.
match goal with
| [ _ : lstepSilent^* pr1' ?x |- _ ] => apply trc_trans with (x || pr2')
end.
eauto.
match goal with
| [ _ : lstepSilent^* pr2' ?x' |- lstepSilent^* (?x || _) _ ] => eapply trc_trans with (x || x')
end.
eauto.
apply trc_one.
eauto.
eauto.
Qed.
Theorem refines_Par : forall pr1 pr2 pr1' pr2',
pr1 <| pr1'
-> pr2 <| pr2'
-> pr1 || pr2 <| pr1' || pr2'.
Proof.
invert 1; invert 1.
exists (RPar x x0).
unfold simulates in *.
propositional; eauto using refines_Par_Silent, refines_Par_Action.
Qed.
(** ** Block *)
(* A few similar properties apply to [Block], too. *)
Inductive RBlock (R : proc -> proc -> Prop) : proc -> proc -> Prop :=
| RBlock1 : forall pr1 pr2 ch,
R pr1 pr2
-> RBlock R (Block ch; pr1) (Block ch; pr2).
Global Hint Constructors RBlock : core.
Global Hint Unfold notUse : core.
Lemma lstepSilent_Block : forall ch pr1 pr2,
lstepSilent^* pr1 pr2
-> lstepSilent^* (Block ch; pr1) (Block ch; pr2).
Proof.
induct 1; eauto.
Qed.
Global Hint Resolve lstepSilent_Block : core.
Theorem refines_Block : forall pr1 pr2 ch,
pr1 <| pr2
-> Block ch; pr1 <| Block ch; pr2.
Proof.
invert 1.
exists (RBlock x).
first_order; eauto.
invert H2.
invert H3.
eapply H in H6; eauto.
first_order.
eauto.
invert H2.
invert H3.
eapply H0 in H6; eauto.
first_order.
eauto 10.
Qed.
Inductive RBlock2 : proc -> proc -> Prop :=
| RBlock2_1 : forall ch1 ch2 pr,
RBlock2 (Block ch1; Block ch2; pr) (Block ch2; Block ch1; pr).
Global Hint Constructors RBlock2 : core.
Theorem refines_Block2 : forall ch1 ch2 pr,
Block ch1; Block ch2; pr <| Block ch2; Block ch1; pr.
Proof.
exists RBlock2.
first_order; eauto.
invert H.
invert H0.
invert H2.
eauto 10.
invert H.
invert H0.
invert H2.
eauto 10.
Qed.
(* This predicate is handy for side conditions, to enforce that a process never
* uses a particular channel for anything. *)
Inductive neverUses (ch : channel) : proc -> Prop :=
| NuRecv : forall ch' (A : Type) (k : A -> _),
ch' <> ch
-> (forall v, neverUses ch (k v))
-> neverUses ch (Recv ch' k)
| NuSend : forall ch' (A : Type) (v : A) k,
ch' <> ch
-> neverUses ch k
-> neverUses ch (Send ch' v k)
| NuDup : forall pr,
neverUses ch pr
-> neverUses ch (Dup pr)
| NuPar : forall pr1 pr2,
neverUses ch pr1
-> neverUses ch pr2
-> neverUses ch (pr1 || pr2)
| NuDone :
neverUses ch Done.
Global Hint Constructors neverUses : core.
Lemma neverUses_step : forall ch pr1,
neverUses ch pr1
-> forall l pr2, lstep pr1 l pr2
-> neverUses ch pr2.
Proof.
induct 1; invert 1; eauto.
Qed.
Global Hint Resolve neverUses_step : core.
Inductive RBlockS : proc -> proc -> Prop :=
| RBlockS1 : forall ch pr1 pr2,
neverUses ch pr2
-> RBlockS (Block ch; pr1 || pr2) ((Block ch; pr1) || pr2).
Global Hint Constructors RBlockS : core.
Lemma neverUses_notUse : forall ch pr l,
neverUses ch pr
-> forall pr', lstep pr l pr'
-> notUse ch l.
Proof.
induct 1; invert 1; simplify; eauto.
Qed.
Lemma notUse_Input_Output : forall ch r,
notUse ch (Action (Input r))
-> notUse ch (Action (Output r)).
Proof.
simplify; auto.
Qed.
Lemma notUse_Output_Input : forall ch r,
notUse ch (Action (Output r))
-> notUse ch (Action (Input r)).
Proof.
simplify; auto.
Qed.
Global Hint Resolve neverUses_notUse : core.
Theorem refines_BlockS : forall ch pr1 pr2,
neverUses ch pr2
-> Block ch; pr1 || pr2 <| (Block ch; pr1) || pr2.
Proof.
exists RBlockS.
first_order; eauto.
invert H0.
invert H1.
invert H4; eauto 10.
eexists; propositional.
apply trc_one.
eapply LStepRendezvousLeft; eauto.
constructor; eauto.
apply notUse_Output_Input; eauto.
eauto.
eexists; propositional.
apply trc_one.
eapply LStepRendezvousRight; eauto.
constructor; eauto.
apply notUse_Input_Output; eauto.
eauto.
invert H0.
invert H1.
invert H4; eauto 10.
Qed.
(** * The first example again *)
(* Those tools will help us lift our earlier adder proof to the immortal-server
* case, without writing any new simulation relations ourselves. *)
Theorem refines_add2 : forall input output,
input <> output
-> add2 input output <| addNs 2 input output.
Proof.
simplify.
apply refines_Dup.
apply add2_once_refines_addN; auto.
Qed.
(* We can even check refinement of our different adders when run together with
* the tester, carefully marking internal channels as private with [Block]. *)
Theorem refines_add2_with_tester : forall metaInput input output metaOutput,
input <> output
-> Block input; Block output; add2 input output || tester metaInput input output metaOutput
<| Block input; Block output; addNs 2 input output || tester metaInput input output metaOutput.
Proof.
simplify.
do 2 apply refines_Block.
apply refines_Par.
apply refines_add2; auto.
apply refines_refl.
Qed.
(** * Tree membership *)
(* Here's one more example of a parallel program, which searches a binary tree
* in parallel, checking if a value is found at one of the leaves. *)
Inductive tree :=
| Leaf (n : nat)
| Node (l r : tree).
(* This function formalizes the membership property that we check. *)
Fixpoint mem (n : nat) (t : tree) : bool :=
match t with
| Leaf m => if m ==n n then true else false
| Node l r => mem n l || mem n r
end%bool.
(* Here's the lame (but straightforward) sequential implementation. Note that
* we do nothing if the value is not found, and we send exactly one [tt] value
* as output if the value is found. *)
Definition inTree_seq (t : tree) (input output : channel) :=
Dup (??input(n : nat);
if mem n t then
!!output(tt);
Done
else
Done).
(* Helper function for a fancier parallel version, creating many threads that
* are all allowed to send to a channel [output], if they find the value. *)
Fixpoint inTree_par' (n : nat) (t : tree) (output : channel) :=
match t with
| Leaf m =>
if m ==n n then
!!output(tt);
Done
else
Done
| Node l r =>
inTree_par' n l output || inTree_par' n r output
end.
(* Top-level wrapper for an immortal-server tree-searcher *)
Definition inTree_par (t : tree) (input output : channel) :=
Dup (??input(n : nat);
New[input;output](output');
inTree_par' n t output'
|| ??output'(_ : unit);
!!output(tt);
Done).
(* Note the second part of the parallel composition, which makes sure we send
* *at most one* notification to the outside world, though the internal threads
* may generate as many notifications as there are tree leaves. *)
(* OK, now we get into the complex part, to prove the simulation. We will let
* the relations and lemmas below "speak for themselves," though admittedly it's
* a pretty involved argument. *)
Inductive TreeThreads (output' : channel) : bool -> proc -> Prop :=
| TtDone : forall maySend,
TreeThreads output' maySend Done
| TtSend :
TreeThreads output' true (!!output'(tt); Done)
| TtPar : forall maySend pr1 pr2,
TreeThreads output' maySend pr1
-> TreeThreads output' maySend pr2
-> TreeThreads output' maySend (pr1 || pr2).
(* This is the main simulation relation. *)
Inductive RTree (t : tree) (input output : channel) : proc -> proc -> Prop :=
| TreeInit :
RTree t input output
(??input(n : nat);
New[input;output](output');
inTree_par' n t output'
|| ??output'(_ : unit);
!!output(tt);
Done)
(??input(n : nat);
if mem n t then
!!output(tt);
Done
else
Done)
| TreeGotInput : forall n,
RTree t input output
(New[input;output](output');
inTree_par' n t output'
|| ??output'(_ : unit);
!!output(tt);
Done)
(if mem n t then
!!output(tt);
Done
else
Done)
| TreeSearching : forall n output' threads,
~In output' [input; output]
-> TreeThreads output' (mem n t) threads
-> RTree t input output
(Block output';
threads
|| ??output'(_ : unit);
!!output(tt);
Done)
(if mem n t then
!!output(tt);
Done
else
Done)
| TreeFound : forall n output' threads,
mem n t = true
-> ~In output' [input; output]
-> TreeThreads output' true threads
-> RTree t input output