-
Notifications
You must be signed in to change notification settings - Fork 11
/
smallstep.v
942 lines (866 loc) · 29.9 KB
/
smallstep.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
(* monae: Monadic equational reasoning in Coq *)
(* Copyright (C) 2020 monae authors, license: LGPL-2.1-or-later *)
Require Import Eqdep JMeq List ssreflect.
Import ListNotations.
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
Require Import hierarchy monad_lib state_lib trace_lib monad_model.
(******************************************************************************)
(* Application of monadTrace to program semantics *)
(* *)
(* Inductive program, Inductive continuation: *)
(* Syntax for an imperative language with a primitive to record execution *)
(* trace *)
(* Section OperationalSemantics, Inductive step: *)
(* A small-step semantics *)
(* DenotationalSemantics: *)
(* Denotation given in terms of the state/trace monad *)
(* Section semantics_equivalence: *)
(*. Prove that the small-step semantics is equivalent to the denotation *)
(* nonce, nonce_twice, countdown, etc. *)
(* Examples of programs using traces and their small-step and denotational *)
(* semantics. *)
(* *)
(* reference: *)
(* - R. Affeldt, D. Nowak, T. Saikawa, A Hierarchy of Monadic Effects for *)
(* Program Verification using Equational Reasoning, MPC 2019 *)
(******************************************************************************)
Set Universe Polymorphism.
Unset Universe Minimization ToSet.
Set Polymorphic Inductive Cumulativity.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Set Bullet Behavior "Strict Subproofs".
Obligation Tactic := idtac.
Reserved Notation "'p_do' x <- m ; e"
(at level 60, x name, m at level 200, e at level 60).
Reserved Notation "'p_do' x : T <- m ; e"
(at level 60, x name, m at level 200, e at level 60).
Section Syntax.
Variables T S : Type.
Inductive program : Type -> Type :=
| p_ret : forall {A}, A -> program A
| p_bind : forall {A B}, program A -> (A -> program B) -> program B
| p_cond : forall {A}, bool -> program A -> program A -> program A
| p_repeat : nat -> program unit -> program unit
| p_while : nat -> (S -> bool) -> program unit -> program unit
| p_get : program S
| p_put : S -> program unit
| p_mark : T -> program unit.
Local Notation "'p_do' x <- m ; e" := (p_bind m (fun x => e)).
Local Notation "'p_do' x : T <- m ; e" :=(p_bind m (fun x : T => e)).
Inductive continuation : Type :=
| stop : forall A, A -> continuation
| cont : forall A, program A -> (A -> continuation) -> continuation.
End Syntax.
Arguments program {_ _} _.
Arguments p_ret {_ _ _} _.
Arguments p_bind {_ _ _ _} _ _.
Arguments p_cond {_ _ _} _ _ _.
Arguments p_repeat {_ _} _ _.
Arguments p_while {_ _} _ _ _.
Arguments p_get {_ _}.
Arguments p_put {_ _} _.
Arguments p_mark {_ _} _.
Arguments continuation {_ _}.
Arguments stop {_ _} _ _.
Arguments cont {_ _} _ _ _.
Notation "'p_do' x <- m ; e" := (@p_bind _ _ _ _ m (fun x => e)).
Notation "'p_do' x : T <- m ; e" := (@p_bind _ _ _ _ m (fun x : T => e)).
Notation "p `; k" := (@cont _ _ _ p k) (at level 50).
Section OperationalSemantics.
Variables T S : Type.
Definition state : Type := S * @continuation T S.
Inductive step : state -> option T -> state -> Prop :=
| s_ret : forall s A a (k : A -> _), step (s, p_ret a `; k) None (s, k a)
| s_bind : forall s A B p (f : A -> program B) k,
step (s, p_bind p f `; k) None (s, p `; fun a => f a `; k)
| s_cond_true : forall s A p1 p2 (k : A -> _),
step (s, p_cond true p1 p2 `; k) None (s, p1 `; k)
| s_cond_false : forall s A p1 p2 (k : A -> _),
step (s, p_cond false p1 p2 `; k) None (s, p2 `; k)
| s_repeat_O : forall s p k, step (s, p_repeat O p `; k) None (s, k tt)
| s_repeat_S : forall s n p k,
step (s, p_repeat n.+1 p `; k) None
(s, p `; fun _ => p_repeat n p `; k)
| s_while_true : forall fuel s c p k, c s = true ->
step (s, p_while fuel.+1 c p `; k) None
(s, p `; fun _ => p_while fuel c p `; k)
| s_while_false : forall fuel s c p k, c s = false ->
step (s, p_while fuel.+1 c p `; k) None (s, k tt)
| s_while_broke : forall s c p k, step (s, p_while O c p `; k) None (s, k tt)
| s_get : forall s k, step (s, p_get `; k) None (s, k s)
| s_put : forall s s' k, step (s, p_put s' `; k) None (s', k tt)
| s_mark : forall s t k, step (s, p_mark t `; k) (Some t) (s, k tt).
Inductive step_n : nat -> state -> list T -> state -> Prop :=
| sn_0 : forall sk, step_n O sk [] sk
| sn_S_None : forall n sk1 sk2 sk3 l,
step sk1 None sk2 -> step_n n sk2 l sk3 ->
step_n n.+1 sk1 l sk3
| sn_S_Some : forall n sk1 sk2 sk3 t l,
step sk1 (Some t) sk2 -> step_n n sk2 l sk3 ->
step_n n.+1 sk1 (t :: l) sk3.
Inductive step_star : state -> list T -> state -> Prop :=
| ss_refl : forall sk, step_star sk [] sk
| ss_step_None : forall sk1 sk2 sk3 l,
step sk1 None sk2 -> step_star sk2 l sk3 -> step_star sk1 l sk3
| ss_step_Some : forall sk1 sk2 sk3 t l,
step sk1 (Some t) sk2 -> step_star sk2 l sk3 -> step_star sk1 (t :: l) sk3.
Lemma step_star_transitive sk1 sk2 sk3 l l' :
step_star sk1 l sk2 -> step_star sk2 l' sk3 -> step_star sk1 (l ++ l') sk3.
Proof.
intro Hss1.
revert sk3 l'.
induction Hss1 as
[ | sk1 sk2 sk3 l Hstep Hss1 IH | sk1 sk2 sk3 t l Hstep Hss1 IH ];
intros sk3' l' Hss2; [ assumption | | ].
- apply ss_step_None with (sk2 := sk2).
+ exact Hstep.
+ apply IH; exact Hss2.
- apply ss_step_Some with (sk2 := sk2).
+ exact Hstep.
+ apply IH; exact Hss2.
Qed.
Lemma step_star_stop_inv s A a l sk :
step_star (s, stop A a) l sk -> l = [] /\ sk = (s, stop A a).
Proof.
intro Hss.
inversion Hss.
- split; reflexivity.
- subst.
match goal with H : step _ _ _ |- _ => inversion H end.
- subst.
match goal with H : step _ _ _ |- _ => inversion H end.
Qed.
Lemma step_deterministic ski l1 l2 sk1 sk2 :
step ski l1 sk1 -> step ski l2 sk2 -> l1 = l2 /\ sk1 = sk2.
Proof.
intro Hstep1.
revert l2 sk2.
induction Hstep1; intros l2 sk2 Hstep2;
match goal with
| _ : step (?s, ?k) _ _ |- _ => remember (s, k) as sk1 eqn: Heq2
end; inversion Hstep2; clear Hstep2; subst; try discriminate;
match goal with
| H : _ = _ |- _ => injection H; clear H; intros
end; subst;
repeat match goal with
| H : existT _ _ _ = existT _ _ _ |- _ => apply inj_pair2 in H
end; subst; repeat split; congruence.
Qed.
Lemma step_star_confluent ski sk1 sk2 l1 l2 :
step_star ski l1 sk1 -> step_star ski l2 sk2 ->
exists l1' l2' skf,
step_star sk1 l1' skf /\ step_star sk2 l2' skf /\ l1 ++ l1' = l2 ++ l2'.
Proof.
intro Hss1.
revert l2 sk2.
induction Hss1 as [
s
| sk1 sk2' sk3 l1 Hstep1 Hss1 IH
| sk1 sk2' sk3 t1 l1 Hstep1 Hss1 IH
].
- intros l2 sk2 Hss2.
exists l2. exists []. exists sk2.
split; [ | split ].
+ exact Hss2.
+ apply ss_refl.
+ rewrite cats0; reflexivity.
- intros l2 sk2 Hss2.
inversion Hss2 as [
sk1' Hsk1 Hl2 Hsk2
| sk1' sk2'' sk2''' l2' Hstep2 Hss2' Hsk1 Hl2 Hsl2
| sk1' sk2'' sk2''' t2 l2' Hstep2 Hss2' Hsk1 Hl2 Hsl2
].
+ subst sk1' l2 sk2.
do 3 eexists.
split; [ apply ss_refl | ].
split; [ eapply ss_step_None; eassumption | ].
rewrite cats0; reflexivity.
+ subst sk1' l2' sk2'''.
specialize (step_deterministic Hstep1 Hstep2).
intros [ [] Heq2].
subst sk2''.
apply IH.
exact Hss2'.
+ subst sk1' l2 sk2'''.
specialize (step_deterministic Hstep1 Hstep2).
intros [ [=] ?].
- intros l2 sk2 Hss2.
inversion Hss2 as [
sk1' Hsk1 Hl2 Hsk2
| sk1' sk2'' sk2''' l2' Hstep2 Hss2' Hsk1 Hl2 Hsl2
| sk1' sk2'' sk2''' t2 l2' Hstep2 Hss2' Hsk1 Hl2 Hsl2
].
+ subst sk1' l2 sk2.
do 3 eexists.
split; [ apply ss_refl | ].
split; [ eapply ss_step_Some; eassumption | ].
rewrite cats0; reflexivity.
+ subst sk1' l2' sk2'''.
specialize (step_deterministic Hstep1 Hstep2).
intros [ [=] ?].
+ subst sk1' l2 sk2'''.
specialize (step_deterministic Hstep1 Hstep2).
intros [ [= Heq1] Heq2].
subst t2 sk2''.
apply IH in Hss2'.
destruct Hss2' as (l1' & l2'' & skf & Hss3 & Hss4 & Heq).
do 3 eexists.
do 2 (split; [ eassumption | ]).
cbn.
f_equal.
exact Heq.
Qed.
Lemma step_star_deterministic ski l1 l2 s1 s2 A1 A2 a1 a2 :
step_star ski l1 (s1, stop A1 a1) -> step_star ski l2 (s2, stop A2 a2) ->
l1 = l2 /\ s1 = s2 /\ A1 = A2 /\ JMeq a1 a2.
Proof.
intros Hss1 Hss2.
specialize (step_star_confluent Hss1 Hss2).
intros (l1' & l2' & skf & Hss1' & Hss2' & Heq).
apply step_star_stop_inv in Hss1'.
apply step_star_stop_inv in Hss2'.
destruct Hss1' as [ Heq11 Heq12 ].
destruct Hss2' as [ Heq21 Heq22 ].
subst l1' l2' skf .
do 2 rewrite cats0 in Heq.
injection Heq22; clear Heq22; intros; subst.
match goal with
| H : existT _ _ _ = existT _ _ _ |- _ => apply inj_pair2 in H
end.
subst.
repeat split.
Qed.
Definition run_s {A : Type} (p : program A) (f : A -> continuation) (s : S) :
{o & {f' & {s' | step (s, p `; f) o (s', f') } } }.
Proof.
destruct p as [ A a | A B p g | A b p1 p2 | n p | fuel c p | | s' | t ];
try (repeat eexists; constructor).
- destruct b; repeat eexists; constructor.
- destruct n; repeat eexists; constructor.
- destruct fuel.
+ repeat eexists; constructor.
+ case_eq (c s); intro Hcs; repeat eexists.
* apply s_while_true.
exact Hcs.
* apply s_while_false.
exact Hcs.
Defined.
Definition run_s_n (n : nat)
{A : Type} (p : program A) (f : A -> continuation) (s : S) :
option {l & {f' & {s' | step_n n (s, p `; f) l (s', f') } } }.
Proof.
revert n A p f s.
fix run_s_n 1.
intros [ | n' ] A p f s.
- apply Some.
exists []. exists (cont A p f). exists s.
apply sn_0.
- destruct (run_s p f s) as (o & [ B b | B p' f' ] & s' & Hstep).
+ destruct n' as [ | n'' ].
* apply Some.
destruct o as [ t | ]; repeat eexists.
-- eapply sn_S_Some.
++ exact Hstep.
++ apply sn_0.
-- eapply sn_S_None.
++ exact Hstep.
++ apply sn_0.
* apply None.
+ destruct (run_s_n n' B p' f' s') as [ (l & f'' & s'' & Hstep_n') | ].
* apply Some.
destruct o as [ t | ]; repeat eexists.
-- eapply sn_S_Some.
++ exact Hstep.
++ exact Hstep_n'.
-- eapply sn_S_None.
++ exact Hstep.
++ exact Hstep_n'.
* exact None.
Defined.
Definition run_gen
{A : Type} (p : program A) (f : A -> continuation) (s : S) :
{l & {a : A & {s' | step_star (s, p `; f) l (s', f a) } } }.
Proof.
revert f s.
induction p as [ A a | A B p IHp g IHg | A b p1 IHp1 p2 IHp2 |
n p IHp | fuel c p IHp | | s' | t ];
intros f s.
- exists []. exists a. exists s.
abstract (eapply ss_step_None; [ apply s_ret | apply ss_refl ]).
- specialize (IHp (fun a => g a `; f) s).
destruct IHp as (l1 & a & s' & Hss1).
specialize (IHg a f s').
destruct IHg as (l2 & b & s'' & Hss2).
exists (l1 ++ l2). exists b. exists s''.
abstract (eapply step_star_transitive; [
eapply ss_step_None; [ apply s_bind | apply Hss1 ]
| exact Hss2
]).
- case b.
+ specialize (IHp1 f s).
destruct IHp1 as (l & a & s' & Hss).
exists l.
exists a.
exists s'.
abstract (eapply ss_step_None; [ apply s_cond_true | apply Hss ]).
+ specialize (IHp2 f s).
destruct IHp2 as (l & a & s' & Hss).
exists l.
exists a.
exists s'.
abstract (eapply ss_step_None; [ apply s_cond_false | apply Hss ]).
- revert s.
induction n as [ | n' IHn ]; intro s.
+ exists []; exists tt; exists s.
abstract (eapply ss_step_None; [ apply s_repeat_O | apply ss_refl ]).
+ destruct (IHp (fun _ => p_repeat n' p `; f) s) as (l1 & a1 & s1 & Hss1).
destruct (IHn s1) as (l2 & a2 & s2 & Hss2).
exists (l1 ++ l2); exists a2; exists s2.
eapply ss_step_None; [ apply s_repeat_S | ].
eapply step_star_transitive; [ eexact Hss1 | exact Hss2 ].
- revert s.
induction fuel as [ | fuel' IHfuel ]; intro s.
+ exists []; exists tt; exists s.
abstract (eapply ss_step_None; [ apply s_while_broke | apply ss_refl ]).
+ case_eq (c s); [ intro Htrue | intro Hfalse ].
* destruct (IHp (fun _ => p_while fuel' c p `; f) s) as (l1 & a1 & s1 & Hss1).
destruct (IHfuel s1) as (l2 & a2 & s2 & Hss2).
exists (l1 ++ l2); exists a2; exists s2.
eapply ss_step_None; [ apply s_while_true; exact Htrue | ].
eapply step_star_transitive; [ eexact Hss1 | exact Hss2 ].
* exists []; exists tt; exists s.
abstract (eapply ss_step_None; [ apply s_while_false; exact Hfalse | apply ss_refl ]).
- exists []. exists s. exists s.
abstract (eapply ss_step_None; [ apply s_get | apply ss_refl ]).
- exists []. exists tt. exists s'.
abstract (eapply ss_step_None; [ apply s_put | apply ss_refl ]).
- exists [t]. exists tt. exists s.
abstract (eapply ss_step_Some; [ apply s_mark | apply ss_refl ]).
Defined.
Definition run_ss {A : Type} (p : program A) (s : S) :
{l & {a : A & {s' |
step_star (s, p `; stop A) l (s', stop A a) } } } :=
run_gen p (stop A) s.
End OperationalSemantics.
Arguments step {_ _} _ _ _.
Arguments step_star {_ _} _ _ _.
Arguments run_s {_ _ _} _ _ _.
Arguments run_s_n {_ _} _ {_} _ _ _.
Arguments run_ss {_ _ _} _ _.
Local Open Scope monae_scope.
Section DenotationalSemantics.
Variables S T : Type.
Variable M : stateTraceMonad S T.
Fixpoint denote {A} (p : program A) : M A :=
match p with
| p_ret _ v => Ret v
| p_bind _ _ m f => denote m >>= (denote \o f)
| p_cond _ b p1 p2 => if b then denote p1 else denote p2
| p_repeat n p => (fix loop m : M unit :=
if m is m'.+1 then denote p >> loop m' else Ret tt) n
| p_while fuel c p => (fix loop m : M unit :=
if m is m'.+1 then
(st_get >>= (fun s =>
if c s then denote p >> loop m' else Ret tt))
else Ret tt) fuel
| p_get => st_get
| p_put s' => st_put s'
| p_mark t => st_mark t
end.
Notation "'Repeat' n {{ p }}" := (
(fix loop (m : nat) : M unit :=
match m with
| 0 => Ret tt
| m'.+1 => denote p >> loop m'
end) n) (at level 200).
Notation "'While' fuel @ c {{ p }}" := (
(fix loop (m : nat) : M unit :=
match m with
| 0 => Ret tt
| m'.+1 =>
st_get >>= (fun s =>
if c s then denote p >> loop m' else Ret tt)
end) fuel) (at level 200).
Fixpoint denote_continuation (k : continuation) : M (@continuation T S) :=
match k with
| stop A a => Ret (stop A a)
| p `; f => denote p >>= (denote_continuation \o f)
end.
Definition stateTrace_sub A (m : M A) : Type :=
{ p | denote p = m }.
Definition continuation_sub (m : M continuation) : Type :=
{k | denote_continuation k = m }.
End DenotationalSemantics.
Arguments denote {S} {T} M A.
Arguments denote_continuation {S} {T} M.
Section semantics_equivalence.
Variables S T : Type.
Variable M : stateTraceReifyMonad S T.
Lemma denote_prefix_preserved A (m : M A) :
stateTrace_sub m -> forall s s' l1 l a,
reify m (s, l1) = Some (a, (s', l)) ->
exists l2, l = l1 ++ l2.
Proof.
case=> p <-{m}.
induction p as [ A a | A B p IHp g IHg | A b p1 IHp1 p2 IHp2 |
n p IHp | fuel c p IHp | | s0 | t ]; cbn;
intros s s' l1 l a' Heq.
- exists [].
rewrite cats0.
by move: Heq; rewrite reifyret => -[].
- rewrite reifybind in Heq.
case_eq (reify (denote M _ p) (s, l1)).
+ intros (a, (s0, l0)) Hp.
rewrite Hp in Heq.
move/IHp : Hp => [l2 Hp].
move/IHg : Heq => [l2' Heq].
exists (l2 ++ l2').
by rewrite Heq Hp catA.
+ intro Hp.
rewrite Hp in Heq.
discriminate Heq.
- destruct b; [ eapply IHp1 | eapply IHp2 ]; exact Heq.
- revert s l1 Heq.
induction n as [ | n' IH ]; intros s l1 Heq.
+ exists [].
rewrite cats0.
by move: Heq; rewrite reifyret => -[].
+ rewrite reifybind in Heq.
case_eq (reify (denote M _ p) (s, l1)).
* intros (a, (s0, l0)) Hp.
move: (IHp _ _ _ _ _ Hp) => [l2 ?].
subst l0.
rewrite Hp in Heq.
move: (IH _ _ Heq) => [l3 ?].
exists (l2 ++ l3).
by rewrite catA.
* intro Hp.
rewrite Hp in Heq.
discriminate Heq.
- revert s l1 Heq.
induction fuel as [ | fuel' IH ]; intros s l1 Heq.
+ exists [].
rewrite cats0.
by move: Heq; rewrite reifyret => -[].
+ rewrite reifybind reifystget in Heq.
simpl in Heq.
destruct (c s).
* rewrite reifybind in Heq.
case_eq (reify (denote M _ p) (s, l1)).
-- intros (a ,(s0, l0)) Hp.
move: (IHp _ _ _ _ _ Hp) => [l2 ?].
subst l0.
rewrite Hp in Heq.
move: (IH _ _ Heq) => [l3 ?].
exists (l2 ++ l3).
by rewrite catA.
-- intro Hp.
rewrite Hp in Heq.
discriminate Heq.
* exists [].
rewrite cats0.
by move: Heq; rewrite reifyret => -[].
- exists [].
rewrite cats0.
by move: Heq; rewrite reifystget => -[].
- exists [].
rewrite cats0.
by move: Heq; rewrite reifystput => -[].
- exists [t].
by move: Heq; rewrite reifystmark -cats1 => -[].
Qed.
Lemma denote_prefix_independent A (m : M A) :
stateTrace_sub m -> forall s l1 l2,
reify m (s, l1 ++ l2) =
let res := reify m (s, l2) in
match res with
| None => None
| Some res => Some (res.1, (res.2.1, l1 ++ res.2.2))
end.
Proof.
intros [ p Hp ] s l1 l2.
subst m.
elim: p s l1 l2 => /= {A} [A a|A B p1 IH1 p2 IH2|A b p1 IH1 p2 IH2|
n p IHp|fuel c p IHp||s'|t] s l1 l2.
- by rewrite !reifyret.
- rewrite [in LHS]reifybind [in LHS]IH1.
rewrite [in RHS]reifybind.
case: (reify (denote M _ p1) (s, l2)) => [[a' [s' l']] | ] /=.
+ by rewrite IH2.
+ reflexivity.
- by case: ifPn => _; [rewrite IH1|rewrite IH2].
- revert s l2.
induction n as [ | n' IH ]; intros s l2.
+ by rewrite !reifyret.
+ do 2 rewrite reifybind.
rewrite {}IHp.
case_eq (reify (denote M _ p) (s, l2)).
* intros (a, (s0, l0)) Hp.
exact: IH.
* reflexivity.
- revert s l2.
induction fuel as [ | fuel' IH ]; intros s l2.
+ by rewrite !reifyret.
+ do 2 rewrite reifybind reifystget.
cbn.
destruct (c s).
* do 2 rewrite reifybind.
rewrite IHp.
clear IHp.
case_eq (reify (denote M _ p) (s, l2)).
-- intros (a, (s0, l0)) Hp.
exact: IH.
-- reflexivity.
* by rewrite !reifyret.
- by rewrite !reifystget.
- by rewrite !reifystput.
- by rewrite !reifystmark rcons_cat.
Qed.
Lemma denote_continuation_prefix_independent (m : M _) :
continuation_sub m -> forall s l1 l2,
reify m (s, l1 ++ l2) =
let res := reify m (s, l2) in
match res with
| None => None
| Some res => Some (res.1, (res.2.1, l1 ++ res.2.2))
end.
Proof.
intros [ k Hk ].
subst m.
elim: k => // [A a s l1 l2|A p k IH s l1 l2].
by rewrite !reifyret.
rewrite /= !reifybind.
rewrite denote_prefix_independent /=; [ | now exists p ].
destruct (reify (denote M _ p) (s, l2)) as [ (a, (s', l)) | ].
- by rewrite IH.
- reflexivity.
Qed.
Lemma step_None_correct s s' k k' l :
step (s, k) None (s', k') ->
reify (denote_continuation M k) (s, l) = reify (denote_continuation M k') (s', l).
Proof.
intro Hstep.
remember (s, k) as sk eqn: Heq.
remember None as o eqn: Heqo.
remember (s', k') as sk' eqn: Heq'.
revert s s' k k' l Heq Heq' Heqo.
induction Hstep as
[ s A a f | s A B p f g | s A p1 p2 k | s A p1 p2 k |
s p k | s n p k | fuel s c p k Htrue | fuel s c p k Hfalse | s c p k |
s f | s s' f | s t f ];
intros s1 s2 k1 k2 l [= Hs1 Hk1] [= Hs2 Hk2] Heqo.
- subst s1 k1 s2 k2.
by rewrite /= reifybind reifyret.
- subst s1 k1 s2 k2.
cbn.
by rewrite bindA.
- subst s1 s2 k1 k2.
reflexivity.
- subst s1 s2 k1 k2.
reflexivity.
- subst.
cbn.
rewrite bindretf.
reflexivity.
- subst.
cbn.
rewrite bindA.
reflexivity.
- subst.
cbn.
rewrite bindA reifybind reifystget Htrue bindA.
reflexivity.
- subst.
cbn.
rewrite bindA reifybind reifystget Hfalse bindretf.
reflexivity.
- subst.
cbn.
rewrite bindretf.
reflexivity.
- subst s1 k1 s2 k2.
by rewrite /= reifybind reifystget.
- subst s1 k1 s2 k2.
by rewrite /= reifybind reifystput.
- discriminate Heqo.
Qed.
Lemma step_Some_correct s s' k k' t l :
step (s, k) (Some t) (s', k') ->
reify (denote_continuation M k) (s, l) =
reify (denote_continuation M k') (s', rcons l t).
Proof.
intro Hstep.
remember (s, k) as sk eqn: Heq.
remember (Some t) as o eqn: Heqo.
remember (s', k') as sk' eqn: Heq'.
revert s s' k k' l Heq Heq' Heqo.
induction Hstep as
[ s A a f | s A B p f g | s A p1 p2 k | s A p1 p2 k |
s p k | s n p k | fuel s c p k Htrue | fuel s c p k Hfalse | s c p k |
s f | s s' f | s t' f ];
intros s1 s2 k1 k2 l [= Hs1 Hk1] [= Hs2 Hk2] Heqo; try discriminate Heqo.
subst s1 k1 s2 k2.
injection Heqo; intro; subst t.
by rewrite /= reifybind reifystmark.
Qed.
Lemma step_star_correct_gen s s' k k' l l' :
step_star (s, k) l' (s', k') ->
reify (denote_continuation M k) (s, l) = reify (denote_continuation M k') (s', l++l').
Proof.
intro Hstep_star.
remember (s, k) as sk eqn: Heq.
remember (s', k') as sk' eqn: Heq'.
revert s s' k k' l Heq Heq'.
induction Hstep_star as
[ s |
(s, k) (s', k') (s'', k'') l' Hstep Hstep_star IH |
(s, k) (s', k') (s'', k'') t l' Hstep Hstep_star IH ];
intros s1 s2 k1 k2 l1 Heq1 Heq2.
- rewrite cats0.
by move: Heq2; rewrite Heq1 => -[<- <-].
- move: Heq1 Heq2 => [<- <-] [<- <-].
apply step_None_correct with (l := l1) in Hstep.
rewrite Hstep.
apply IH; reflexivity.
- move: Heq1 Heq2 => [<- <-] [<- <-].
apply step_Some_correct with (l := []) in Hstep.
rewrite <- cats0 at 1.
rewrite denote_continuation_prefix_independent; [ | now exists k ].
rewrite -> Hstep, (IH _ s'' _ k'');
[ | reflexivity | reflexivity ].
cbn.
rewrite denote_continuation_prefix_independent; [ reflexivity | ].
now eexists.
Qed.
Proposition step_star_correct
(s s' : S) (A : Type) (a : A) (p : program A) (l : list T) :
step_star (s, p `; stop A) l (s', stop A a) ->
reify (denote M _ p) (s, []) = Some (a, (s', l)).
Proof.
intro Hss.
apply step_star_correct_gen with (l := []) in Hss.
move: Hss.
rewrite /= reifyret reifybind.
destruct (reify (denote M _ p) (s, [])) as [[a'' [s'' l'']] | ].
- rewrite reifyret => -[Heq3 <- <-].
apply inj_pair2 in Heq3.
by rewrite Heq3.
- discriminate.
Qed.
Lemma step_star_complete_gen
(s s' : S) (A : Type) (a : A) (p : program A) (l1 l2 : list T) f :
reify (denote M _ p) (s, l1) = Some (a, (s', l1 ++ l2)) ->
step_star (s, p `; f) l2 (s', f a).
Proof.
revert s s' a l1 l2 f.
induction p as [ A a | A B p IHp g IHg | A b p1 IHp1 p2 IHp2 |
n p IHp | fuel c p IHp | | s0' | t ]; cbn;
intros s s' a' l1 l2 f Heq.
- rewrite reifyret in Heq.
injection Heq; clear Heq; intros; subst a' s'.
replace l2 with (@nil T) by
(revert l2 H; induction l1; [ tauto | intros ? [=]; firstorder ]).
eapply ss_step_None; [ apply s_ret | apply ss_refl ].
- eapply ss_step_None.
+ apply s_bind.
+ move: Heq.
rewrite reifybind.
case_eq (reify (denote M _ p) (s, l1)).
intros (a, (s0, l0)) Hp Heq.
move: (denote_prefix_preserved ltac:(now eexists) Hp) => [l3 Hl3].
rewrite Hl3 in Hp.
apply IHp with (f := (fun a => g a `; f)) in Hp.
clear IHp.
move: (denote_prefix_preserved ltac:(now eexists) Heq) => [l4 Hl4].
rewrite Hl4 in Heq.
apply IHg with (f := f) in Heq.
clear IHg.
subst l0.
replace l2 with (l3 ++ l4) by
(induction l1; cbn in Hl4; [ congruence | injection Hl4; tauto ]).
eapply step_star_transitive.
* exact Hp.
* exact Heq.
* discriminate.
- destruct b; [
eapply ss_step_None; [
apply s_cond_true
| apply IHp1 with (l1 := l1); exact Heq ]
| eapply ss_step_None; [
apply s_cond_false
| apply IHp2 with (l1 := l1); exact Heq ]
].
- revert s l1 l2 Heq.
induction n as [ | n' IHn ]; intros s l1 l2 Heq.
+ rewrite reifyret in Heq.
injection Heq; clear Heq; intros; subst a' s'.
replace l2 with (@nil T) by
(revert l2 H; induction l1; [ tauto | intros ? [=]; firstorder ]).
eapply ss_step_None; [ apply s_repeat_O | apply ss_refl ].
+ rewrite reifybind in Heq.
case_eq (reify (denote M _ p) (s, l1)).
* intros (a, (s0, l0)) Hp.
rewrite Hp in Heq.
move: (denote_prefix_preserved ltac:(now eexists) Hp) => [l3 Hl3].
rewrite Hl3 {l0 Hl3} in Hp, Heq.
specialize (IHp _ _ _ _ _ (fun _ => p_repeat n' p `; f) Hp).
assert (Heq':
reify (denote M _ (p_repeat n' p)) (s0, l1 ++ l3) = Some (a', (s', l1 ++ l2)))
by apply Heq.
move: (denote_prefix_preserved ltac:(now eexists) Heq') => [l4 Hl4].
rewrite Hl4 in Heq.
eapply ss_step_None; [ apply s_repeat_S | ].
have -> : l2 = l3 ++ l4.
by move/(congr1 (drop (size l1))) : Hl4; rewrite -catA ?drop_size_cat.
eapply step_star_transitive; [ eexact IHp | eapply IHn; eexact Heq ].
* intro Hp.
rewrite Hp in Heq.
discriminate.
- revert s l1 l2 Heq.
induction fuel as [ | fuel' IHn ]; intros s l1 l2 Heq.
+ rewrite reifyret in Heq.
injection Heq; clear Heq; intros; subst a' s'.
replace l2 with (@nil T) by
(revert l2 H; induction l1; [ tauto | intros ? [=]; firstorder ]).
eapply ss_step_None; [ apply s_while_broke | apply ss_refl ].
+ rewrite reifybind reifystget in Heq.
cbn in Heq.
case_eq (c s); [ intro Htrue | intro Hfalse ].
* rewrite Htrue reifybind in Heq.
case_eq (reify (denote M _ p) (s, l1)).
-- intros (a, (s0, l0)) Hp.
rewrite Hp in Heq.
move: (denote_prefix_preserved ltac:(now eexists) Hp) => [l3 Hl3].
rewrite Hl3 {l0 Hl3} in Hp, Heq.
specialize (IHp _ _ _ _ _ (fun _ => p_while fuel' c p `; f) Hp).
assert (Heq':
reify (denote M _ (p_while fuel' c p)) (s0, l1 ++ l3) = Some (a', (s', l1 ++ l2)))
by apply Heq.
move: (denote_prefix_preserved ltac:(now eexists) Heq') => [l4 Hl4].
rewrite Hl4 in Heq.
eapply ss_step_None; [ apply s_while_true; exact Htrue | ].
have -> : l2 = l3 ++ l4.
by move/(congr1 (drop (size l1))) : Hl4; rewrite -catA ?drop_size_cat.
eapply step_star_transitive; [ eexact IHp | eapply IHn; eexact Heq ].
-- intro Hp.
rewrite Hp in Heq.
discriminate.
* move: Heq; rewrite Hfalse reifyret.
move=> [<- <-] /(congr1 (drop (size l1))).
rewrite drop_size_cat // drop_size => <-.
eapply ss_step_None; [ apply s_while_false; exact Hfalse | apply ss_refl ].
- move: Heq; rewrite reifystget.
move=> [<- <-] /(congr1 (drop (size l1))).
rewrite drop_size_cat // drop_size => <-.
eapply ss_step_None; [ apply s_get | apply ss_refl ].
- move: Heq; rewrite reifystput.
move=> [<- <-] /(congr1 (drop (size l1))).
rewrite drop_size_cat // drop_size => <-.
eapply ss_step_None; [ apply s_put | apply ss_refl ].
- move: Heq; rewrite reifystmark.
move=> [<- <-] /(congr1 (drop (size l1))).
rewrite drop_size_cat // drop_rcons // drop_size => <-.
eapply ss_step_Some; [ apply s_mark | apply ss_refl ].
Qed.
Proposition step_star_complete
(s s' : S) (A : Type) (a : A) (p : program A) (l : list T) :
reify (denote M _ p) (s, []) = Some (a, (s', l)) ->
step_star (s, p `; stop A) l (s', stop A a).
Proof.
intro Hp.
apply step_star_complete_gen with (l1 := []).
exact Hp.
Qed.
End semantics_equivalence.
Notation "'eT' x y" := (@existT _ _ x y) (at level 200).
Notation "'e' x" := (@exist _ _ x _) (at level 200).
Definition p_nonce : program nat :=
p_do n <- p_get;
p_do _ <- p_put (S n);
p_do _ <- p_mark n;
p_ret n.
(*Definition M := @ModelStateTraceReify.mk.*)
Eval unfold denote, p_nonce in denote _ nat p_nonce.
Local Open Scope do_notation.
Definition nonce : (StateMonad.acto (nat * seq nat)%type) nat :=
do n : nat <- st_get;
do _ : unit <- st_put (S n);
do _ : unit <- st_mark n;
Ret n.
Compute nonce (0, []).
Compute (denote ([the stateTraceMonad nat nat of (StateMonad.acto (nat * seq nat)%type)]) nat p_nonce) (0, []).
Compute run_ss p_nonce 0.
Remark denote_p_nonce : denote _ nat p_nonce = nonce.
Proof. by []. Qed.
Program Example p_nonce_twice : program bool :=
p_do nonce <- p_ret (
p_do n : nat <- p_get;
p_do _ : unit <- p_put (S n);
p_do _ : unit <- p_mark n;
p_ret n ) ;
p_do x <- nonce ;
p_do y <- nonce ;
p_ret (x == y).
Example nonce_twice : [the stateTraceMonad nat nat of (StateMonad.acto (nat * seq nat)%type)] _ :=
do nonce <- Ret (
do n : nat <- st_get;
do _ : unit <- st_put (S n);
do _ : unit <- st_mark n;
Ret n ) ;
do x <- nonce ;
do y <- nonce ;
Ret (Nat.eqb x y).
Compute nonce_twice (0, []).
Compute (denote ([the stateTraceMonad nat nat of (StateMonad.acto (nat * seq nat)%type)]) bool p_nonce_twice) (0, []).
Compute run_ss p_nonce_twice 0.
Remark denote_p_nonce_twice :
denote _ bool p_nonce_twice = nonce_twice.
Proof. by []. Qed.
Fixpoint countdown (fuel : nat) : [the stateTraceMonad nat bool of (StateMonad.acto (nat * seq bool)%type)] unit :=
match fuel with
| O => Ret tt
| S fuel' =>
do n <- st_get ;
if (n == 0) then
st_mark true
else
do _ <- st_mark false ; do _ <- st_put (n-1) ; countdown fuel'
end.
Fixpoint p_countdown (fuel : nat) : program unit :=
match fuel with
| O => p_ret tt
| S fuel' =>
p_do n <- p_get ;
p_cond (n == 0) (
p_mark true
) (
p_do _ <- p_mark false ; p_do _ <- p_put (n-1) ; p_countdown fuel'
)
end.
Compute (countdown 100) (5, []).
Compute (denote [the stateTraceMonad nat bool of (StateMonad.acto (nat * seq bool)%type)] unit (p_countdown 100)) (5, []).
Compute run_ss (p_countdown 100) 5.
Remark denote_countdown fuel :
denote ([the stateTraceMonad nat bool of (StateMonad.acto (nat * seq bool)%type)]) unit (p_countdown fuel) = countdown fuel.
Proof.
elim: fuel => // n.
rewrite [countdown (S n)]/=.
by move <-.
Qed.
Example p_multiply (a b : nat) : program (T := unit) unit :=
p_do _ <- p_put 0 ;
p_repeat b (
p_do x <- p_get ;
p_put (a + x)
).
Compute run_ss (p_multiply 3 7) 0.
Example p_division (a b : nat) : program (T := unit) unit :=
p_do _ <- p_put (a, 0);
p_while a (fun s => b <= fst s) (
p_do s <- p_get ;
p_put (fst s - b, S (snd s))
).
Compute run_ss (p_division 22 7) (0, 0).
Compute run_s_n 15 (p_division 22 7) (stop unit) (0, 0).