-
Notifications
You must be signed in to change notification settings - Fork 0
/
NIProof.v
1624 lines (1559 loc) · 77.2 KB
/
NIProof.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
Require Import Coq.Strings.String.
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype.
From mathcomp Require Import finset path fingraph. (* These depend on Mathematical Components 1.5
http://www.msr-inria.fr/projects/mathematical-components-2/ *)
Require Import Utils Labels Rules Memory Instructions Machine Indist NotionsOfNI.
Require Import Omega.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Set Bullet Behavior "Strict Subproofs".
Module NIProof (Lattice : FINLAT).
Module GenericMachine := MachineM Lattice.
Export GenericMachine.
Module GenericIndist := IndistM Lattice.
Export GenericIndist.
(* Interface with non-ssr definitions *)
Lemma replicateE T (a : T) n : replicate a n = nseq n a.
Proof.
by elim: n=> //= n ->.
Qed.
Definition def_atom := Vint 0 @ ⊥.
Lemma nth_errorE T l n (a def : T) : List.nth_error l n = Some a ->
nth def l n = a /\ n < size l.
Proof.
by elim: l n => [[]|x l IHl [[->]|]].
Qed.
Lemma nth_error_ZE T l n (a def : T) : nth_error_Z l n = Some a ->
nth def l (BinInt.Z.to_nat n) = a /\ BinInt.Z.to_nat n < size l.
Proof.
by rewrite /nth_error_Z; case: (BinInt.Z.ltb n 0) => //; apply: nth_errorE.
Qed.
Lemma update_listE T r r' (def : T) rk a : update_list r rk a = Some r' ->
r' = set_nth def r rk a /\ rk < size r.
Proof.
elim: r rk r' => // x l IHl [r' [<-]|rk] // [|y r'] /=.
by case: (update_list l rk a)=> //.
case H: (update_list l rk a) => [a'|] //; case=> <- <-.
by split; case: (IHl rk a') => // <-.
Qed.
Lemma update_list_ZE r r' rk a : update_list_Z r rk a = Some r' ->
r' = set_nth def_atom r (BinInt.Z.to_nat rk) a /\
BinInt.Z.to_nat rk < size r.
Proof.
rewrite /update_list_Z; case: (BinInt.Z.ltb rk 0)=> //.
exact: update_listE.
Qed.
(* TODO: prove once mframe is actually made finite *)
Axiom f : mframe -> ordinal (2^32).
Axiom g : ordinal (2^32) -> mframe.
Axiom fgK : cancel f g.
Canonical label_eqType : eqType := Eval hnf in (@LabelEqType.label_eqType _ _).
Axiom label_choiceMixin : choiceMixin Label.
Canonical label_choiceType := Eval hnf in ChoiceType Label label_choiceMixin.
Axiom label_countMixin : Countable.mixin_of Label.
Canonical label_countType := Eval hnf in CountType Label label_countMixin.
(* TODO: prove using the assumptions in FINLAT *)
Axiom label_enumP : Finite.axiom (undup elems).
Definition label_finMixin := FinMixin label_enumP.
Canonical label_finType := Eval hnf in FinType Label label_finMixin.
Definition mframe_eqMixin := CanEqMixin fgK.
Canonical mframe_eqType := Eval hnf in EqType mframe mframe_eqMixin.
Definition mframe_choiceMixin := CanChoiceMixin fgK.
Canonical mframe_choiceType := Eval hnf in ChoiceType mframe mframe_choiceMixin.
Definition mframe_countMixin := CanCountMixin fgK.
Canonical mframe_countType := Eval hnf in CountType mframe mframe_countMixin.
Definition mframe_finMixin := CanFinMixin fgK.
Canonical mframe_finType := Eval hnf in FinType mframe mframe_finMixin.
Canonical block_eqType := Eval hnf in EqType (Mem.block Label) mframe_eqMixin.
Canonical block_choiceType := Eval hnf in ChoiceType (Mem.block Label) mframe_choiceMixin.
Canonical block_countType := Eval hnf in CountType (Mem.block Label) mframe_countMixin.
Canonical block_finType := Eval hnf in FinType (Mem.block Label) mframe_finMixin.
Definition is_low_pointer obs (a : Atom) : bool :=
if a is Vptr p @ l then isLow l obs else false.
Definition extract_mframe (a : Atom) : option mframe :=
if a is Vptr (Ptr fp _) @ _ then Some fp else None.
Definition mframes_from_atoms obs (atoms : list Atom) : {set mframe} :=
[set t in pmap extract_mframe (filter (is_low_pointer obs) atoms)].
Lemma mframes_from_atoms_nth r r1 fp i lbl obs :
registerContent r r1 = Some (Vptr (Ptr fp i) @ lbl) -> isLow lbl obs ->
fp \in mframes_from_atoms obs r.
Proof.
case/(nth_error_ZE def_atom) => get_r1 lt_r1 low_lbl.
rewrite inE mem_pmap; apply/mapP.
exists (Vptr (Ptr fp i) @ lbl) => //.
by rewrite mem_filter /= low_lbl -get_r1 mem_nth.
Qed.
Lemma mem_set_nth (T : eqType) (x : T) x0 l i v :
i < size l -> x \in set_nth x0 l i v ->
x = v \/ x \in l.
Proof.
move=> /maxn_idPr eq_size /(nthP x0) [j].
rewrite nth_set_nth size_set_nth /= => lt_j <-.
have [_|_] := altP (j =P i); first by left.
by right; rewrite mem_nth // -eq_size.
Qed.
Lemma mframes_from_atoms_upd obs r rk r' atom :
registerUpdate r rk atom = Some r' ->
mframes_from_atoms obs r' \subset mframes_from_atoms obs r :|: mframes_from_atoms obs [:: atom].
Proof.
case/update_list_ZE => ->; set k := BinInt.Z.to_nat rk => lt_k.
rewrite /mframes_from_atoms; apply/subsetP=> x; rewrite !inE /= !mem_pmap.
case/mapP=> a; rewrite mem_filter; case/andP => low_pt.
move/(mem_set_nth lt_k)=> // [<- ->|a_in_r ->].
by rewrite [X in _ || X]map_f ?orbT // low_pt inE.
by rewrite map_f // mem_filter low_pt.
Qed.
Arguments mframes_from_atoms_upd [obs r rk r' atom] _.
Fixpoint root_set_stack obs (s : list StackFrame) : {set mframe} :=
match s with
| nil => set0
| (SF pc rs _ _) :: s' =>
if isLow ∂pc obs then
mframes_from_atoms obs rs :|: root_set_stack obs s'
else root_set_stack obs s'
end.
Definition root_set_registers obs (r : regSet) pcl :=
if isLow pcl obs then mframes_from_atoms obs r
else set0.
Lemma root_set_registers_nth r r1 fp i lbl obs pcl :
registerContent r r1 = Some (Vptr (Ptr fp i) @ lbl) ->
isLow pcl obs -> isLow lbl obs ->
fp \in root_set_registers obs r pcl.
Proof.
move=> get_r1 low_pcl low_lbl; rewrite /root_set_registers low_pcl.
exact: (mframes_from_atoms_nth get_r1).
Qed.
Lemma root_set_registers_upd obs pcl r rk r' atom :
registerUpdate r rk atom = Some r' ->
root_set_registers obs r' pcl \subset root_set_registers obs r pcl :|: mframes_from_atoms obs [:: atom].
Proof.
rewrite /root_set_registers.
case: ifP => _; first exact: mframes_from_atoms_upd.
by rewrite sub0set.
Qed.
Arguments root_set_registers_upd [obs pcl r rk r' atom] _.
Lemma joinC : commutative join.
Proof.
move=> l1 l2.
by apply/flows_antisymm; rewrite join_minimal ?flows_join_left ?flows_join_right.
Qed.
Lemma flows_join l1 l2 l : flows (l1 \_/ l2) l = flows l1 l && flows l2 l.
Proof.
case Hl1: (flows l1 l).
case Hl2: (flows l2 l).
by rewrite (join_minimal _ _ _ Hl1 Hl2).
by rewrite joinC (not_flows_not_join_flows_left _ _ _ Hl2).
by rewrite (not_flows_not_join_flows_left _ _ _ Hl1).
Qed.
Lemma low_join l1 l2 l : isLow (l1 \_/ l2) l = isLow l1 l && isLow l2 l.
Proof. exact: flows_join. Qed.
Lemma joinA : associative join.
Proof.
(* Cannot use wlog because of missing type class resolution *)
have: forall l1 l2 l3, l1 \_/ (l2 \_/ l3) <: (l1 \_/ l2) \_/ l3.
move=> l1 l2 l3.
rewrite flows_join.
apply/andP; split; first exact/join_1/join_1/flows_refl.
rewrite flows_join.
apply/andP; split; first exact/join_1/join_2/flows_refl.
exact/join_2/flows_refl.
move=> H l1 l2 l3.
apply/flows_antisymm; first exact:H.
rewrite [_ \_/ l3]joinC [l2 \_/ l3]joinC [l1 \_/ l2]joinC.
by rewrite [l1 \_/ (_ \_/ _)]joinC; apply: H.
Qed.
Lemma root_set_registers_join obs r l1 l2 :
root_set_registers obs r (l1 \_/ l2) = root_set_registers obs r l1 :&: root_set_registers obs r l2.
Proof.
rewrite /root_set_registers /=.
rewrite low_join.
case: (isLow l1 obs); last by rewrite set0I.
case: (isLow l2 obs); first by rewrite setIid.
by rewrite setI0.
Qed.
Definition root_set obs (st : State) : {set mframe} :=
let '(St _ _ s r pc) := st in
root_set_registers obs r ∂pc :|: root_set_stack obs (unStack s).
Definition link obs (mem : memory) (f1 f2 : mframe) :=
if Mem.get_frame mem f1 is Some (Fr l atoms) then
isLow l obs && (f2 \in mframes_from_atoms obs atoms)
else false.
Definition reachable obs (mem : memory) : rel mframe :=
connect (link obs mem).
Definition well_stamped_label (st : State) (l : Label) :=
forall f1 f2, f1 \in root_set l st -> reachable l (st_mem st) f1 f2 ->
isLow (Mem.stamp f2) l.
Definition well_stamped (st : State) :=
forall l, well_stamped_label st l.
Lemma stamp_alloc μ μ' sz lab stamp i li fp :
alloc sz lab stamp (Vint i@li) μ = Some (fp, μ') ->
Mem.stamp fp = stamp.
Proof.
rewrite /alloc /zreplicate.
case: (ZArith_dec.Z_lt_dec sz 0) => // lt0sz [alloc_sz].
by rewrite (Mem.alloc_stamp alloc_sz).
Qed.
Lemma reachable_alloc_int μ μ' sz lab stamp i li fp l f1 f2 :
alloc sz lab stamp (Vint i@li) μ = Some (fp, μ') ->
reachable l μ' f1 f2 = reachable l μ f1 f2.
Proof.
rewrite /alloc /zreplicate.
case: (ZArith_dec.Z_lt_dec sz 0) => // lt0sz /= [alloc_sz].
apply/eq_connect=> x y.
rewrite /link.
have [<-|neq_fpx] := fp =P x.
(* How about using implicit arguments? *)
rewrite (alloc_get_frame_eq _ _ _ _ _ _ alloc_sz) inE /=.
rewrite (Mem.alloc_get_fresh alloc_sz).
set s := filter _ _.
suff /eqP->: s == [::] by rewrite andbF.
by rewrite -[_ == _]negbK -has_filter has_nseq andbF.
by rewrite (alloc_get_frame_neq _ _ _ _ _ _ _ alloc_sz neq_fpx).
Qed.
Arguments reachable_alloc_int [μ μ' sz lab stamp i li fp l f1 f2] _.
Lemma reachable_upd μ μ' pv lf fr l f1 f2 :
Mem.upd_frame μ pv (Fr lf fr) = Some μ' ->
reachable l μ' f1 f2 -> reachable l μ f1 f2
\/ isLow lf l /\ reachable l μ f1 pv
/\ exists f3, f3 \in mframes_from_atoms l fr /\ reachable l μ f3 f2.
Proof.
(* TODO: use splitPl with pv *)
move=> upd_pv /connectP [p] /(@shortenP _ _ f1) [p'].
have link_not_pv: forall (f : mframe), pv != f -> link l μ' f =1 link l μ f.
move=> f; rewrite eq_sym => /eqP neq_pv f'; rewrite /link.
by rewrite (get_frame_upd_frame_neq upd_pv neq_pv).
have path_not_pv: forall (p : seq mframe) f, pv \notin belast f p -> path (link l μ') f p = path (link l μ) f p.
elim=> //= x s IHs f.
rewrite inE negb_or.
case/andP => neq_pv ?.
by rewrite IHs // link_not_pv.
have [in_path|] := boolP (pv \in f1 :: p').
case/(@splitPl _ f1 p'): in_path => p1 [|f3 p2 last_p1].
rewrite cats0 => last_p1 path_p1 uniq_p1 _ ->; left; apply/connectP.
exists p1 => //; rewrite -path_not_pv //.
by move: uniq_p1; rewrite lastI last_p1 rcons_uniq => /andP [].
rewrite cat_path last_p1 -cat_cons [f1 :: p1]lastI last_p1 cat_uniq last_cat.
rewrite rcons_uniq.
case/andP=> path_p1 path_p2 /and3P [/andP [? _] not_pv _] _ /= ->; right.
rewrite /= {1}/link (get_frame_upd_frame_eq upd_pv) in path_p2.
case/andP: path_p2 => /andP [low_lf ref_f3] path_p2; split=> //; split.
by apply/connectP; exists p1=> //; rewrite -path_not_pv.
exists f3; split => //; apply/connectP; exists p2 => //.
rewrite -path_not_pv //; apply/negP=> pv_in_p2; case/negP: not_pv.
apply/(@sub_has _ (pred1 pv)).
by move=> ? /= /eqP ->; rewrite mem_rcons inE eqxx.
by rewrite has_pred1 lastI mem_rcons inE pv_in_p2 orbT.
rewrite lastI mem_rcons inE negb_or=> /andP [_ ?] path_p' _ _ ->; left.
by apply/connectP; exists p' => //; rewrite -path_not_pv.
Qed.
Lemma well_stamped_preservation st st' : well_stamped st ->
step default_table st st' -> well_stamped st'.
Proof.
move=> wf_st step.
move: wf_st.
case: {st st'} step.
(* Lab *)
+ move=> im μ σ v K pc r r' r1 r2 j LPC rl rpcl -> ? ? [<- <-] upd_r2 wf_st l f1 f2.
move: wf_st => /(_ l f1 f2) /= wf_st.
rewrite inE.
case/orP=> [|in_stack_f1].
move/(subsetP (root_set_registers_upd upd_r2)).
rewrite inE.
case/orP=> [in_regs_f1|].
by rewrite inE in_regs_f1 in wf_st; apply: wf_st.
by rewrite inE.
by rewrite inE in_stack_f1 orbT in wf_st; apply: wf_st.
(* PcLab *)
+ move=> im μ σ pc r r' r1 j LPC rl rpcl -> ? [<- <-] upd_r1 wf_st l f1 f2.
move: wf_st => /(_ l f1 f2) /= wf_st.
rewrite inE.
case/orP=> [|in_stack_f1].
move/(subsetP (root_set_registers_upd upd_r1)).
rewrite inE.
case/orP=> [in_regs_f1|].
by rewrite inE in_regs_f1 in wf_st; apply: wf_st.
by rewrite inE.
by rewrite inE in_stack_f1 orbT in wf_st; apply: wf_st.
(* MLab *)
+ move=> im μ σ pc r r1 r2 p K C j LPC rl r' rpcl -> ? ? get_r1 [].
rewrite /Vector.nth_order /= => <- <- upd_r2 wf_st l f1 f2.
move: wf_st => /(_ l f1 f2) /= wf_st.
rewrite inE.
case/orP=> [|in_stack_f1].
move/(subsetP (root_set_registers_upd upd_r2)).
rewrite inE.
case/orP=> [in_regs_f1|].
by rewrite inE in_regs_f1 in wf_st; apply: wf_st.
by rewrite inE.
by rewrite inE in_stack_f1 orbT in wf_st; apply: wf_st.
(* PutLab *)
+ move=> im μ σ pc r r' r1 j LPC rl rpcl l' -> ? [<- <-] upd_r1 wf_st l f1 f2.
move: wf_st => /(_ l f1 f2) /= wf_st.
rewrite inE.
case/orP=> [|in_stack_f1].
move/(subsetP (root_set_registers_upd upd_r1)).
rewrite inE.
case/orP=> [in_regs_f1|].
by rewrite inE in_regs_f1 in wf_st; apply: wf_st.
by rewrite inE.
by rewrite inE in_stack_f1 orbT in wf_st; apply: wf_st.
(* Call *)
+ move=> im μ σ pc B K r r1 r2 r3 j La addr Lpc rl rpcl -> ? get_r1 get_r2 [<- <-] wf_st l f1 f2.
rewrite /Vector.nth_order /=.
move: wf_st => /(_ l f1 f2) /= wf_st.
rewrite root_set_registers_join !inE; case/orP.
by case/andP=> _ in_regs_f1; apply: wf_st; rewrite inE in_regs_f1.
rewrite low_join.
case: ifPn=> [/andP [_ low_Lpc]|_ in_stack_f1].
by rewrite /root_set_registers low_Lpc in wf_st *.
by rewrite inE in_stack_f1 orbT in wf_st; apply: wf_st.
(* BRet *)
+ move=> im μ σ pc a r r' r'' r1 R pc' B j j' LPC LPC' rl rpcl -> -> ? get_r1.
rewrite /run_tmr /apply_rule /= /Vector.nth_order /=.
case: ifPn=> // Hjoins [<- <-] upd_r1 wf_st l f1 f2 /=.
move: wf_st => /(_ l f1 f2) /=.
rewrite !inE => wf_st.
case/orP=> [|in_stack_f1].
rewrite /root_set_registers; case: ifP => low_LPC'; last by rewrite inE.
move/(subsetP (mframes_from_atoms_upd upd_r1)).
rewrite inE; case/orP=> [in_r'_f1|].
by rewrite low_LPC' inE in_r'_f1 orbT in wf_st; apply: wf_st.
case: a get_r1 upd_r1 => [?|[fp i]|?] get_r1 upd_r1; rewrite /mframes_from_atoms /= !inE //.
case: ifP=> // low_B.
rewrite /= inE => /eqP eq_f1.
move: wf_st.
rewrite eq_f1 (root_set_registers_nth get_r1); first exact.
exact/(join_2_rev R)/(flows_trans _ _ _ Hjoins)/join_minimal.
exact/(join_1_rev R LPC)/(flows_trans _ _ _ Hjoins)/join_minimal.
by case: (isLow LPC' l) wf_st; rewrite ?inE in_stack_f1 !orbT; apply.
(* Alloc *)
+ move=> im μ μ' σ pc r r' r1 r2 r3 i K Ll K' rl rpcl j LPC dfp -> ? get_r1 get_r2 [<- <-] alloc_i.
move: (alloc_i); rewrite /alloc.
case: (zreplicate i (Vint 0 @ ⊥)) => // ? [malloc].
rewrite /Vector.nth_order /= => upd_r3 wf_st l f1 f2.
move: wf_st => /(_ l f1 f2) /=.
rewrite (reachable_alloc_int alloc_i) !inE => wf_st.
case/orP=> [|in_stack_f1].
rewrite /root_set_registers.
case: ifP => low_LPC; last by rewrite inE.
move/(subsetP (mframes_from_atoms_upd upd_r3)).
rewrite inE.
case/orP=> [in_r_f1|].
by move: wf_st; rewrite /root_set_registers low_LPC in_r_f1; apply.
rewrite /mframes_from_atoms /=.
case low_KK': (isLow (K \_/ K') l); last by rewrite inE.
rewrite /= !inE => /eqP ->.
case/connectP=> [[_ ->|]] /=.
by rewrite (stamp_alloc alloc_i) /= joinA low_join low_KK' low_LPC.
move=> a s.
by rewrite /link /= (Mem.alloc_get_fresh malloc).
by move: wf_st; rewrite in_stack_f1 orbT; apply.
(* Load *)
+ move=> im μ σ pc C [pv pl] K r r' r1 r2 j LPC v Ll rl rpcl -> ? get_r1 load_p mlab_p [<- <-].
rewrite /Vector.nth_order /= => upd_r2 wf_st l f1 f2 /=.
rewrite inE; case/orP=> [|in_stack_f1].
rewrite /root_set_registers.
case: ifP; last by rewrite inE.
rewrite !low_join; case/and3P=> low_LPC low_K low_C.
move/(subsetP (mframes_from_atoms_upd upd_r2)).
rewrite inE; case/orP=> [in_r_f1|].
by apply: wf_st; rewrite inE /root_set_registers low_LPC in_r_f1.
rewrite inE /=; case: v load_p upd_r2 => // [[fp ?]] load_p upd_r2.
case low_Ll: (isLow Ll l) => //=.
rewrite !inE.
move/eqP=> -> reach_f2.
apply: (wf_st l pv f2); first by rewrite inE (root_set_registers_nth get_r1).
apply/(connect_trans _ reach_f2)/connect1; move: load_p mlab_p.
rewrite /link /=; case: (Mem.get_frame μ pv) => // [[? fr]] get_pl [->].
apply/andP; split=> //.
exact: (mframes_from_atoms_nth get_pl).
by apply: wf_st; rewrite inE in_stack_f1 orbT.
(* Store *)
+ move=> im μ σ pc v [fp i] μ' r r1 r2 j LPC rpcl rl lp lf lv -> ? get_r1 get_r2 /= lab_p.
rewrite /run_tmr /= /apply_rule /= /Vector.nth_order /=.
case: ifP => //; rewrite flows_join; case/andP => low_lp_lf low_LPC_lf [<- <-].
case get_fp: (Mem.get_frame μ fp) lab_p => // [[? fr]] [eq_lf].
rewrite eq_lf in get_fp *.
case upd_i: (update_list_Z fr i (v @ lv)) => [fr'|] // upd_fp wf_st l f1 f2.
rewrite inE /= => H.
case/(reachable_upd upd_fp) => [|[low_lf [reach_fp [f3 []]]]].
by apply: wf_st; rewrite inE.
move/(subsetP (mframes_from_atoms_upd upd_i)); rewrite inE.
case/orP=> [in_fr_f3 reach_f2|].
apply: (wf_st l f1 f2) => /=; first by rewrite inE.
apply/(connect_trans reach_fp)/(connect_trans _ reach_f2)/connect1.
by rewrite /link get_fp low_lf.
case: v get_r2 upd_i => [|[pv pi] get_r2 upd_i|]; rewrite /mframes_from_atoms /= ?inE //.
case: ifP => // low_lv; rewrite inE => /eqP ->; apply: wf_st.
rewrite inE /= /root_set_registers (root_set_registers_nth get_r2) //.
exact/(flows_trans _ _ _ low_LPC_lf).
(* Write *)
+ move=> im μ σ pc v [fp i] μ' r r1 r2 j LPC rpcl rl v' lp lv lv' lf -> ? get_r1 get_r2 /= load_fp lab_fp.
rewrite /run_tmr /= /apply_rule /= /Vector.nth_order /=.
case: ifP => //; rewrite !flows_join=> /andP [/andP [low_LPC low_lp] low_lv] [<- <-].
case get_fp: (Mem.get_frame μ fp) lab_fp => // [[? fr]] [eq_lf].
rewrite eq_lf in get_fp *.
case upd_i: (update_list_Z fr i (v @ lv')) => [fr'|] // upd_fp wf_st l f1 f2.
rewrite inE /= => H.
case/(reachable_upd upd_fp) => [|[low_lf [reach_fp [f3 []]]]].
by apply: wf_st; rewrite inE.
move/(subsetP (mframes_from_atoms_upd upd_i)); rewrite inE.
case/orP=> [in_fr_f3 reach_f2|].
apply: (wf_st l f1 f2) => /=; first by rewrite inE.
apply/(connect_trans reach_fp)/(connect_trans _ reach_f2)/connect1.
by rewrite /link get_fp low_lf.
case: v get_r2 upd_i => [|[pv pi] get_r2 upd_i|]; rewrite /mframes_from_atoms /= ?inE //.
case: ifP => // low_lv'; rewrite inE => /eqP ->; apply: wf_st.
rewrite inE /= /root_set_registers (root_set_registers_nth get_r2) //.
by apply/(flows_trans _ _ _ low_LPC); rewrite flows_join low_lv' low_lf.
by apply/(flows_trans _ _ _ low_lv); rewrite flows_join low_lv' low_lf.
(* Jump *)
+ move=> im μ σ pc addr Ll r r1 j LPC rpcl -> ? get_r1 [<-] wf_st l f1 f2.
rewrite /Vector.nth_order /= root_set_registers_join !inE.
case/orP=> [/andP [in_regs_f1 _]|in_stack_f1]; apply: wf_st; rewrite inE.
by rewrite in_regs_f1.
by rewrite in_stack_f1 orbT.
(* BNZ *)
+ move=> im μ σ pc n m K r r1 j LPC rpcl -> ? get_r1 [<-] wf_st l f1 f2.
rewrite /Vector.nth_order /= root_set_registers_join !inE.
case/orP=> [/andP [_ in_regs_f1]|in_stack_f1]; apply: wf_st; rewrite inE.
by rewrite in_regs_f1.
by rewrite in_stack_f1 orbT.
(* PSetOff *)
+ move=> im μ σ pc fp' j K1 n K2 r r' r1 r2 r3 j' LPC rl rpcl -> ? get_r1 get_r2 [<- <-].
rewrite /Vector.nth_order /= => upd_r3 wf_st l f1 f2.
rewrite inE; case/orP=> [|in_stack_f1] /=.
rewrite /root_set_registers; case: ifP => // low_LPC; last by rewrite inE.
move/(subsetP (mframes_from_atoms_upd upd_r3)).
rewrite inE; case/orP=> [in_regs_f1|] /=.
by apply: wf_st; rewrite inE /root_set_registers low_LPC in_regs_f1.
rewrite inE /= low_join.
case: ifP => //= /andP [? ?].
rewrite inE => /eqP ->.
apply: wf_st.
rewrite inE.
rewrite (root_set_registers_nth get_r1) //.
by apply: wf_st; rewrite inE in_stack_f1 orbT.
(* Put *)
+ move=> im μ σ pc x r r' r1 j LPC rl rpcl -> ? [<- <-] upd_r1 wf_st l f1 f2.
rewrite inE; case/orP=> [|in_stack_f1] /=.
move/(subsetP (root_set_registers_upd upd_r1)).
rewrite inE; case/orP=> [in_regs_f1|].
by apply: wf_st; rewrite inE in_regs_f1.
by rewrite !inE.
by apply: wf_st; rewrite inE in_stack_f1 orbT.
(* BinOp *)
+ move=> im μ σ pc o v1 L1 v2 L2 v r r1 r2 r3 r' j LPC rl rpcl -> _ get_r1 get_r2 [<- <-] eval.
rewrite /Vector.nth_order /= => upd_r3 wf_st l f1 f2.
rewrite inE; case/orP=> [|in_stack_f1].
move/(subsetP (root_set_registers_upd upd_r3)).
rewrite inE; case/orP=> [in_regs_f1|] /=.
by apply: wf_st; rewrite inE in_regs_f1.
by case: o eval; case: v1 get_r1 => ? ; case: v2 get_r2 => ? //= _ _ [<-]; rewrite !inE.
by apply: wf_st; rewrite inE in_stack_f1 orbT.
(* Nop *)
+ move=> im μ σ pc r j LPC rpcl -> _ [<-] wf_st l f1 f2.
exact: wf_st.
(* MSize *)
+ move=> im μ σ pc p K C r r' r1 r2 j LPC rl rpcl n -> _ get_r1 lab_p [<- <-] size_p.
rewrite /Vector.nth_order /= => upd_r2 wf_st l f1 f2.
rewrite inE; case/orP=> [|in_stack_f1].
rewrite root_set_registers_join inE; case/andP=> in_regs_f1 _.
move/(subsetP (root_set_registers_upd upd_r2)): in_regs_f1.
rewrite inE; case/orP=> [in_regs_f1|] /=.
by apply: wf_st; rewrite inE in_regs_f1.
by rewrite inE.
by apply: wf_st; rewrite inE in_stack_f1 orbT.
(* PGetOff *)
+ move=> im μ σ pc fp' j K r r' r1 r2 j' LPC rl rpcl -> _ get_r1 [<- <-].
rewrite /Vector.nth_order /= => upd_r2 wf_st l f1 f2.
rewrite inE; case/orP=> [|in_stack_f1].
move/(subsetP (root_set_registers_upd upd_r2)).
rewrite inE; case/orP=> [in_regs_f1|] /=.
by apply: wf_st; rewrite inE in_regs_f1.
by rewrite inE.
by apply: wf_st; rewrite inE in_stack_f1 orbT.
(* Mov *)
+ move=> im μ σ v K pc r r' r1 r2 j LPC rl rpcl -> _ get_r1 [<- <-].
rewrite /Vector.nth_order /= => upd_r2 wf_st l f1 f2.
rewrite inE; case/orP=> [|in_stack_f1].
rewrite /root_set_registers; case: ifP => low_LPC; last by rewrite inE.
move/(subsetP (mframes_from_atoms_upd upd_r2)).
rewrite inE; case/orP=> [in_regs_f1|] /=.
by apply: wf_st; rewrite inE /root_set_registers low_LPC in_regs_f1.
case: v get_r1 upd_r2 => [|[? ?]|] get_r1 upd_r2; try by rewrite inE.
rewrite inE /=; case: ifP => // low_K /=; rewrite inE=> /eqP ->.
apply: wf_st; rewrite inE /root_set_registers low_LPC.
by rewrite (mframes_from_atoms_nth get_r1).
by apply: wf_st; rewrite inE in_stack_f1 orbT.
Qed.
Lemma indist_low_pc obs st1 st2 :
isLow ∂(st_pc st1) obs ->
indist obs st1 st2 =
[&& indist obs (st_imem st1) (st_imem st2),
indist obs (st_mem st1) (st_mem st2),
indist obs (st_stack st1) (st_stack st2),
st_pc st1 == st_pc st2 &
indist obs (st_regs st1) (st_regs st2)].
Proof.
case: st1 => im1 mem1 stk1 regs1 pc1; case: st2 => im2 mem2 stk2 regs2 pc2.
rewrite /GenericIndist.indist /=.
by move => -> /=; do 3!bool_congr.
Qed.
Lemma indist_instr obs st1 st2 :
indist obs st1 st2 ->
isLow ∂(st_pc st1) obs ->
state_instr_lookup st1 = state_instr_lookup st2.
Proof.
move => Hindist Hlow.
rewrite (indist_low_pc _ Hlow) in Hindist.
rewrite /state_instr_lookup.
by case/and5P: Hindist => /eqP -> _ _ /eqP -> _.
Qed.
Lemma indist_registerContent_aux obs rs1 rs2 r :
indist obs rs1 rs2 ->
indist obs (registerContent rs1 r) (registerContent rs2 r).
Proof.
rewrite /registerContent.
rewrite /indist /indistList /nth_error_Z.
case: (BinInt.Z.ltb r 0) => //=.
elim: {r} (BinInt.Z.to_nat r) rs1 rs2
=> [|n IH] [|x xs] [|y ys] //=.
- by case/and3P.
- move/(_ xs ys) in IH; rewrite eqSS; case/and3P=> Hs _ H.
by apply: IH; rewrite Hs H.
Qed.
Lemma indist_registerContent obs st1 st2 r v1 :
indist obs st1 st2 ->
isLow ∂(st_pc st1) obs ->
registerContent (st_regs st1) r = Some v1 ->
exists2 v2,
registerContent (st_regs st2) r = Some v2 &
indist obs v1 v2.
Proof.
move => Hindist Hlow.
rewrite (indist_low_pc _ Hlow) in Hindist.
case/and5P: Hindist => _ _ _ _.
move => Hindist Hdef.
move: (indist_registerContent_aux r Hindist).
rewrite Hdef.
case: (registerContent (st_regs st2) r) => [v2|] //=.
by eauto.
Qed.
Lemma indist_registerUpdate_aux obs rs1 rs2 r v1 v2 :
indist obs rs1 rs2 ->
indist obs v1 v2 ->
indist obs (registerUpdate rs1 r v1) (registerUpdate rs2 r v2).
Proof.
rewrite /registerUpdate /update_list_Z.
case: (BinInt.Z.ltb r 0) => //=.
elim: {r} (BinInt.Z.to_nat r) rs1 rs2
=> [|n IH] [|x xs] [|y ys] //=.
- rewrite /indist /= /indist /indistList //= /indist.
by rewrite eqSS; move => /and3P [-> _ ->] /= ->.
- rewrite /indist /= /indist /indistList /= eqSS.
move/and3P => [Hs Hxy Hxsys] Hv1v2.
move: IH Hxy => /(_ xs ys); rewrite Hs Hxsys => /(_ erefl Hv1v2) {Hxsys Hv1v2}.
case: (update_list xs n v1) => [xs'|]; case: (update_list ys n v2) => [ys'|] //=.
rewrite /indist /= /indistList /indist eqSS.
by case/andP=> [-> ->] /= ->.
Qed.
Lemma indist_registerUpdate obs st1 st2 r v1 v2 regs1 :
indist obs st1 st2 ->
isLow ∂(st_pc st1) obs ->
indist obs v1 v2 ->
registerUpdate (st_regs st1) r v1 = Some regs1 ->
exists2 regs2,
registerUpdate (st_regs st2) r v2 = Some regs2 &
indist obs regs1 regs2.
Proof.
move => Hindist Hlow.
move: Hindist.
rewrite indist_low_pc // => /and5P [_ _ _ _ Hindist] Hv1v2 Hupd.
move: (indist_registerUpdate_aux r Hindist Hv1v2).
rewrite Hupd.
case: (registerUpdate (st_regs st2) r v2) => [regs2|] //=.
by eauto.
Qed.
Lemma indist_pc obs st1 st2 :
indist obs st1 st2 ->
isLow ∂(st_pc st1) obs ->
st_pc st1 = st_pc st2.
Proof.
by move=> i l; case/and3P: i=> [_ _]; rewrite l /= => /and3P [/eqP ->].
Qed.
Lemma pc_eqS pc pc' l1 l2 :
(PAtm (BinInt.Z.add pc 1) l1 == PAtm (BinInt.Z.add pc' 1) l2) =
(PAtm pc l1 == PAtm pc' l2).
Proof.
by apply/eqP/eqP=> [[? ->]|[-> ->] //]; congr PAtm; omega.
Qed.
Lemma indist_pcl obs st1 st2 :
indist obs st1 st2 ->
isLow ∂(st_pc st1) obs = isLow ∂(st_pc st2) obs.
Proof.
case/and3P=> [_ _].
have [low1|high1] := boolP (isLow _ _)=> /=.
by case/and4P=> [/eqP <-]; rewrite low1.
have [low2|high2] := boolP (isLow _ _)=> //=.
by case/and4P=> [/eqP e _ _ _]; move: high1; rewrite e low2.
Qed.
Lemma high_low obs s s' :
fstep default_table s = Some s' ->
isHigh ∂(st_pc s) obs ->
isLow ∂(st_pc s') obs ->
state_instr_lookup s = Some BRet.
Proof.
case/fstepP.
(* Lab *)
- by move=> im μ σ v K pc r r' r1 r2 j LPC rl rpcl -> /= instr get_r1 [<- <-] upd_r2 /negbTE ->.
(* PcLab *)
- by move=> im μ σ pc r r' r1 j LPC rl rpcl -> /= CODE [<- <-] upd_r1 /negbTE ->.
(* MLab *)
- by move=> im μ σ pc r r1 r2 p K C j LPC rl r' rpcl -> ? ? get_r1 [] /= _ <- _ /negbTE ->.
(* PutLab *)
- by move=> im μ σ pc r r' r1 j LPC rl rpcl l' -> ? [<- <-] upd_r1 /= /negbTE ->.
(* Call *)
- move=> im μ σ pc B K r r1 r2 r3 j La addr Lpc rl rpcl -> ? get_r1 get_r2 [<- <-].
by rewrite /= flows_join andbC => /negbTE ->.
(* BRet *)
- move=> im μ σ pc a r r' r'' r1 R pc' B j j' LPC LPC' rl rpcl -> -> /= CODE get_r1.
by rewrite /state_instr_lookup /=.
(* Alloc *)
- by move=> im μ μ' σ pc r r' r1 r2 r3 i K Ll K' rl rpcl j LPC dfp -> ? _ _ [<- <-] _ _ /= /negbTE ->.
(* Load *)
- move=> im μ σ pc C [pv pl] K r r' r1 r2 j LPC v Ll rl rpcl -> ? get_r1 load_p mlab_p [<- <-].
rewrite /Vector.nth_order /= => upd_r2.
by rewrite !flows_join => /negbTE ->.
(* Store *)
- move=> im μ σ pc v [fp i] μ' r r1 r2 j LPC rpcl rl lp lf lv -> ? get_r1 get_r2 /= lab_p.
rewrite /run_tmr /= /apply_rule /= /Vector.nth_order /=.
case: ifP => //; rewrite flows_join; case/andP => low_lp_lf low_LPC_lf [<- <-].
by move=> _ /negbTE ->.
(* Write *)
- move=> im μ σ pc v [fp i] μ' r r1 r2 j LPC rpcl rl v' lp lv lv' lf -> ? get_r1 get_r2 /= load_fp lab_fp.
rewrite /run_tmr /= /apply_rule /= /Vector.nth_order /=.
case: ifP => //; rewrite !flows_join=> /andP [/andP [low_LPC low_lp] low_lv] [<- <-].
by move=> _ /negbTE ->.
(* Jump *)
- move=> im μ σ pc addr Ll r r1 j LPC rpcl -> ? get_r1 [<-] /=.
by rewrite flows_join => /negbTE ->.
(* BNZ *)
- move=> im μ σ pc n m K r r1 j LPC rpcl -> ? get_r1 [<-] /=.
by rewrite flows_join andbC => /negbTE ->.
(* PSetOff *)
- move=> im μ σ pc fp' j K1 n K2 r r' r1 r2 r3 j' LPC rl rpcl -> ? get_r1 get_r2 [<- <-] /=.
by move=> _ /negbTE ->.
(* Put *)
- by move=> im μ σ pc x r r' r1 j LPC rl rpcl -> ? [<- <-] upd_r1 /= /negbTE ->.
(* BinOp *)
- move=> im μ σ pc op v1 L1 v2 L2 v r r1 r2 r3 r' j LPC rl rpcl -> _ get_r1 get_r2 [<- <-] eval.
by move=> _ /= /negbTE ->.
(* Nop *)
- by move=> im μ σ pc r j LPC rpcl -> _ [<-] /= /negbTE ->.
(* MSize *)
- move=> im μ σ pc p K C r r' r1 r2 j LPC rl rpcl n -> _ get_r1 lab_p [<- <-] size_p _ /=.
by rewrite flows_join => /negbTE ->.
(* PGetOff *)
- by move=> im μ σ pc fp' j K r r' r1 r2 j' LPC rl rpcl -> _ get_r1 [<- <-] /= _ /negbTE ->.
(* Mov *)
- by move=> im μ σ v K pc r r' r1 r2 j LPC rl rpcl -> _ get_r1 [<- <-] /= _ /negbTE ->.
Qed.
Arguments indist : simpl never.
Theorem SSNI : ssni well_stamped (fstep default_table) (fun obs st => isLow ∂(st_pc st) obs) (indist).
Proof.
constructor=> [obs s1 s2 s1' s2' wf_s1 wf_s2 low_pc indist_s1s2 /fstepP step1|o s1 s1' wf_s1 /= high_pc1 high_pc2 /fstepP step1|o s1 s2 s1' s2' wf_s1 wf_s2 /= high_pc1 indist_s1s2 low_pc1' low_pc2' /fstepP step1].
- case: step1 low_pc indist_s1s2 wf_s1.
(* Lab *)
+ move=> im μ σ v K pc regs1 regs1' r1 r2 j LPC rl rpcl -> instr get_r1 [<- <-] upd_r2 low_pc indist_s1s2 wf_s1.
rewrite /= in instr.
rewrite /fstep -(indist_instr indist_s1s2) /state_instr_lookup //= instr /=.
case: s2 wf_s2 indist_s1s2 => im2 μ2 σ2 regs2 [pcv2 pcl2] wf_s2 indist_s1s2.
have /= [[v2 lv2] -> /andP [/eqP <-]] :=
indist_registerContent indist_s1s2 low_pc get_r1.
have /= [regs2' -> indist_regs _ [<-]] :=
indist_registerUpdate indist_s1s2 low_pc (indistxx (Vlab K @ ⊥)) upd_r2.
rewrite /indist /=; case/and3P: indist_s1s2.
by rewrite indist_regs low_pc pc_eqS !andbT => /= -> -> /= /and3P [-> -> _].
(* PcLab *)
+ move=> im μ σ pc r r' r1 j LPC rl rpcl -> /= CODE [<- <-] upd_r1 low_pc indist_s1s2 wf_s1.
rewrite /fstep -(indist_instr indist_s1s2) /state_instr_lookup //= CODE /=.
case: s2 wf_s2 indist_s1s2 => im2 μ2 σ2 regs2 [pcv2 pcl2] wf_s2 indist_s1s2.
have /= [_ eq_pc] := indist_pc indist_s1s2 low_pc.
rewrite -eq_pc in indist_s1s2 *.
have /= [? -> indist_r' [<-]] :=
indist_registerUpdate indist_s1s2 low_pc (indistxx (Vlab LPC @ ⊥)) upd_r1.
rewrite /indist /=; case/and3P: indist_s1s2.
by rewrite indist_r' low_pc pc_eqS !andbT => /= -> -> /= /and3P [-> -> _].
(* MLab *)
+ move=> im μ σ pc r r1 r2 p K C j LPC rl r' rpcl -> /= CODE mlab_p get_r1 [].
rewrite /Vector.nth_order /= => <- <- upd_r2 low_pc indist_s1s2 wf_s1.
rewrite /fstep -(indist_instr indist_s1s2) /state_instr_lookup //= CODE /=.
case: s2 wf_s2 indist_s1s2 => im2 μ2 σ2 regs2 [pcv2 pcl2] wf_s2 indist_s1s2.
have /= [[[] // p2 lv2] -> // /andP [/eqP <- indist_ptr] {lv2}] :=
indist_registerContent indist_s1s2 low_pc get_r1.
case mlab_p2: mlab => [C2|] //=; rewrite /Vector.nth_order /=.
have indist_v: indist obs (Vlab C @ K) (Vlab C2 @ K).
rewrite /indist /= eqxx /= /indist /indistValue /eq_op /=.
move: indist_ptr mlab_p2; have [K_low|//] //= := boolP (flows K obs).
move=> /eqP [<-] {p2}.
case/and3P: indist_s1s2=> /= [_ /andP [/allP im1m2 _] _] mlab_p2.
case: p mlab_p mlab_p2 get_r1 => [b off] /=.
case get_b: (Mem.get_frame μ b) => [[C' vs]|] //= [e]; subst C'.
case get_b2: (Mem.get_frame μ2 b) => [[C2' vs2]|] //= [e] get_r1; subst C2'.
have b_low: flows (Mem.stamp b) obs.
apply: (wf_s1 obs b b).
apply/setUP; left.
by apply/(root_set_registers_nth get_r1).
by rewrite /reachable /= connect0.
have /(im1m2 _) {im1m2}: b \in blocks_stamped_below obs μ.
apply/Mem.get_blocks_spec.
by rewrite get_b andbT /allThingsBelow mem_filter all_elems andbT.
by rewrite get_b get_b2 /indist /= /indist /= => /andP [].
have /= [? -> indist_r' [<-]] := indist_registerUpdate indist_s1s2 low_pc indist_v upd_r2.
rewrite /indist /=; case/and3P: indist_s1s2.
by rewrite indist_r' low_pc pc_eqS !andbT => /= -> -> /= /and3P [-> -> _].
(* PutLab *)
+ move=> im μ σ pc r r' r1 j LPC rl rpcl l' -> /= CODE [<- <-] upd_r1 low_pc indist_s1s2 wf_s1.
rewrite /fstep -(indist_instr indist_s1s2) /state_instr_lookup //= CODE /=.
case: s2 wf_s2 indist_s1s2 => im2 μ2 σ2 regs2 [pcv2 pcl2] wf_s2 indist_s1s2.
have indist_v: indist obs (Vlab l' @ ⊥) (Vlab l' @ ⊥).
by rewrite /indist /= eqxx /indist /indistValue eqxx orbT.
have /= [? -> indist_r' [<-]] := indist_registerUpdate indist_s1s2 low_pc indist_v upd_r1.
rewrite /indist /=; case/and3P: indist_s1s2.
by rewrite indist_r' low_pc pc_eqS !andbT => /= -> -> /= /and3P [-> -> _].
(* Call *)
+ move=> im μ σ pc B K r r1 r2 r3 j La addr Lpc rl rpcl -> /= CODE get_r1 get_r2 [<- <-] low_pc indist_s1s2 wf_s1.
rewrite /Vector.nth_order /=.
rewrite /fstep -(indist_instr indist_s1s2) /state_instr_lookup //= CODE /=.
case: s2 wf_s2 indist_s1s2 => im2 μ2 σ2 regs2 [pcv2 pcl2] wf_s2 indist_s1s2.
have /= [[[] // ? ? -> // /andP [/eqP <- indist_addr]]] :=
indist_registerContent indist_s1s2 low_pc get_r1.
have /= [[] // [] // ? ? -> // /andP [/eqP <- indist_B] [<-]] :=
indist_registerContent indist_s1s2 low_pc get_r2.
rewrite /Vector.nth_order /=.
rewrite /indist /=; case/and3P: indist_s1s2.
rewrite low_pc => -> -> /= /and3P [/eqP [<- <-] indist_stack indist_r].
rewrite orbb low_join low_pc andbT.
case: ifP indist_addr => /= [low_La /eqP [<-]|hi_La _].
rewrite eqxx /= indist_r andbT /indist /= /indist /= eqSS.
case/andP: indist_stack => [-> ->]; rewrite andbT /=.
rewrite /indist /= orbb flows_join low_pc andbT !eqxx indist_r /=.
by rewrite implybE.
rewrite /cropTop /= flows_join low_pc andbT.
case: (boolP (isLow K obs)) indist_B=> [low_K|hi_K _] /=.
move/eqP=> [<-]; rewrite indist_cons; apply/andP; split=> //.
by rewrite /indist /= orbb indist_r !eqxx /= implybT.
case: (σ) (σ2) indist_stack => [s] [s2]; rewrite {1}/indist /=.
elim: s s2=> [|[[rpc1 rpcl1] rs1 rr1 rl1] st1 IH] [|[[rpc2 rpcl2] rs2 rr2 rl2] st2] //=.
rewrite indist_cons {1}/indist /= implybE negb_or.
case/andP=> [/orP [/andP [H1 H2]|E] Hindist]; move/(_ _ Hindist) in IH.
by rewrite (negbTE H1) (negbTE H2); eauto.
case/and4P: E => [/eqP [-> ->] Hrs /eqP -> /eqP ->].
case: ifP=> //= low2; rewrite indist_cons Hindist andbT.
by rewrite /indist /= low2 !eqxx Hrs.
(* BRet *)
+ move=> im μ σ pc a r r' r'' r1 R pc' B j j' LPC LPC' rl rpcl -> -> /= CODE get_r1.
rewrite /run_tmr /apply_rule /= /Vector.nth_order /=.
case: ifPn=> // Hjoins [<- <-] upd_r1 low_pc indist_s1s2 wf_s1.
rewrite /fstep -(indist_instr indist_s1s2) /state_instr_lookup //= CODE /=.
case: s2 wf_s2 indist_s1s2 => [im2 μ2 [[|sf σ2]] r2 [j2 LPC2]] //=.
case: sf=> [[j2' LPC2'] r2' r12 B2] wf_s2 indist_s1s2.
move: indist_s1s2 (indist_s1s2) wf_s2.
rewrite {1}indist_low_pc //= {3}/indist /=.
case/and5P => [indist_im indist_μ indist_s /eqP [<- <-] {j2 LPC2} indist_r].
move: indist_s; rewrite indist_cons {1}/indist /= => /andP [indist_sf indist_s].
case get_r12: (registerContent r2 r12) => [[a2 R2]|] //= indist_s1s2 wf_s2.
rewrite /run_tmr /apply_rule /= /Vector.nth_order /=.
case: ifPn=> // Hjoins2.
case upd_r12: (registerUpdate _ _ _)=> [r2''|] //= [<-].
rewrite /indist /= indist_im indist_μ /=.
move: indist_sf; case: ifPn=> /=.
move=> low_pc' ind; move: low_pc' indist_s1s2 get_r12 wf_s2 upd_r12 Hjoins2.
case/and4P: ind=> [/eqP [<- <-] indist_r' /eqP <- /eqP <-] {j2' LPC2' r12 B2}.
rewrite orbb=> low_pc' indist_s1s2 get_r12.
move: (indist_registerContent_aux r1 indist_r)=> /=.
rewrite get_r1 get_r12 eqxx /= => /andP [/eqP eR indist_a].
rewrite -{}eR {R2} in get_r12 *; rewrite {1}/indist /= indist_s /=.
move=> wf_s2 upd_r12 _.
have [low|hi] := boolP (isLow B obs).
move: Hjoins indist_a; rewrite flows_join => /andP [lowR _].
rewrite (flows_trans _ _ _ lowR) /= => [indist_a|].
have {indist_a} indist_a : indist obs (a @ B) (a2 @ B).
by rewrite /indist /= eqxx low.
move: (indist_registerUpdate_aux r1 indist_r' indist_a).
by rewrite upd_r1 upd_r12.
by rewrite flows_join low.
have {indist_a} indist_a : indist obs (a @ B) (a2 @ B).
by rewrite /indist /= eqxx hi.
move: (indist_registerUpdate_aux r1 indist_r' indist_a).
by rewrite upd_r1 upd_r12.
move=> _ _.
elim: σ σ2 indist_s {indist_s1s2 wf_s1 wf_s2}=> [|sf σ IH] [|sf2 σ2] //=.
case: sf sf2=> {j' j2' LPC' LPC2' Hjoins Hjoins2 r' r2' upd_r1 upd_r12 r1 r12 get_r1 get_r12}
[[j' LPC'] r' r1 L] [[j2' LPC2'] r2' r12 L2].
rewrite !cropTop_cons indist_cons {1}/indist /=.
have [low /= /andP [Hind Hind_s]|/norP [/negbTE -> /negbTE ->] Hind_s] := boolP (isLow _ _ || isLow _ _).
case/and4P: Hind low=> [/eqP [<- <-] hr hr1 hL] {LPC2'}.
rewrite orbb => low; rewrite low /= indist_cons {1}/indist /= low /= Hind_s andbT.
by apply/and4P; split.
by auto.
(* Alloc *)
+ move=> im μ μ' σ pc rs rs' r1 r2 r3 i K Ll K' rl rpcl j LPC dfp -> /= CODE
get_r1 get_r2 [<- <-] alloc_i.
move: alloc_i get_r1; rewrite /alloc /zreplicate.
case: (ZArith_dec.Z_lt_dec i 0) => [//|Pi] /=.
have {Pi} Pi: BinInt.Z.le 0 i by omega.
rewrite -{2}(Znat.Z2Nat.id _ Pi) {Pi}.
move: (BinInt.Z.to_nat i) => {i} i [Halloc] get_r1.
rewrite /Vector.nth_order /= => upd_r3 low_pc indist_s1s2 wf_s1.
move: (indist_s1s2); rewrite (indist_low_pc) //= => indist_s1s2'.
rewrite /fstep -(indist_instr indist_s1s2) /state_instr_lookup //= CODE /=.
case: s2 wf_s2 indist_s1s2 indist_s1s2'
=> [im2 μ2 σ2 rs2 [j2 LPC2]] //= wf_s2 indist_s1s2 indist_s1s2'.
have /= [[[] // i2 K2 -> // /andP [/eqP <- indist_i]]] :=
indist_registerContent indist_s1s2 low_pc get_r1.
have /= [[[] // Ll2 K2' -> // /andP [/eqP <- indist_Ll]]] :=
indist_registerContent indist_s1s2 low_pc get_r2.
move=> alloc_i2; move: alloc_i2 indist_i.
rewrite /alloc /zreplicate.
case: ZArith_dec.Z_lt_dec=> [//|Pi2] /=.
have {Pi2} Pi2: BinInt.Z.le 0 i2 by omega.
rewrite -{2}(Znat.Z2Nat.id _ Pi2) {Pi2}.
move: (BinInt.Z.to_nat i2) => {i2} i2.
case Halloc2: Mem.alloc=> [dfp2 μ2'].
rewrite /Vector.nth_order /=.
case upd_r32: registerUpdate => [rs2'|] //= [<-] {s2'} indist_i.
case/and5P: indist_s1s2' indist_s1s2 wf_s2 Halloc2
=> [indist_im indist_μ indist_σ /eqP [<- <-] {j2 LPC2} indist_rs]
indist_s1s2 wf_s2 Halloc2.
rewrite /indist /= low_pc indist_im /= eqxx indist_σ /=.
have P1: forall μ1 μ2 μ1' μ2' L1 L2 dfp1 dfp2 fr1 fr2,
indistMemAsym obs μ1 μ2 ->
isHigh L1 obs -> isHigh L2 obs ->
Mem.alloc Local μ1 L1 fr1 = (dfp1,μ1') ->
Mem.alloc Local μ2 L2 fr2 = (dfp2,μ2') ->
indistMemAsym obs μ1' μ2'.
move=> {μ μ' μ2 μ2' dfp dfp2 Halloc Halloc2 wf_s1 wf_s2 indist_μ indist_s1s2 upd_r3 upd_r32}.
move=> μ1 μ2 μ1' μ2' L1 L2 dfp1 dfp2 fr1 fr2 /allP ind hi1 hi2 H1 H2.
apply/allP=> b.
rewrite /blocks_stamped_below -Mem.get_blocks_spec /allThingsBelow mem_filter all_elems.
rewrite andbT (Mem.alloc_get_frame H1) => /andP [low_b].
rewrite (Mem.alloc_get_frame H2).
move: low_b; have [<-{b}|] := altP (dfp1 =P b).
by rewrite (Mem.alloc_stamp H1) (negbTE hi1).
have [<-{b}|ne1 ne2 low_b get_b] := altP (dfp2 =P b).
by rewrite (Mem.alloc_stamp H2) (negbTE hi2).
apply: ind.
rewrite /blocks_stamped_below /allThingsBelow -Mem.get_blocks_spec.
by rewrite mem_filter all_elems low_b.
case: (boolP (isLow K obs)) indist_i => [low_K /= /eqP Hi|hi_K _] /=.
move: Hi Halloc2=> [/Znat.Nat2Z.inj <- {i2}] Halloc2.
case: (boolP (isLow K' obs)) indist_Ll => [low_K' /= /eqP [Hl]|hi_K' _].
rewrite -{}Hl {Ll2} in Halloc2.
have e: dfp = dfp2.
rewrite -[dfp]/(dfp, μ').1 -[dfp2]/(dfp2,μ2').1 -Halloc -Halloc2.
apply: Mem.alloc_local => b Hb.
apply/(sameP idP)/(iffP idP).
case get_b: Mem.get_frame=> [fr|] //= _.
case/andP: indist_μ=> [_ /allP indist_μ].
have /(indist_μ b) : b \in blocks_stamped_below obs μ2.
rewrite /blocks_stamped_below -Mem.get_blocks_spec get_b.
rewrite /allThingsBelow mem_filter all_elems Hb.
by rewrite !flows_join low_K low_K' low_pc.
by rewrite get_b; case: Mem.get_frame.
case get_b: Mem.get_frame=> [fr|] //= _.
case/andP: indist_μ=> [/allP indist_μ _].
have /(indist_μ b) : b \in blocks_stamped_below obs μ.
rewrite /blocks_stamped_below -Mem.get_blocks_spec get_b.
rewrite /allThingsBelow mem_filter all_elems Hb.
by rewrite !flows_join low_K low_K' low_pc.
by rewrite get_b; case: Mem.get_frame.
subst dfp2.
have ind: indist obs (Vptr (Ptr dfp 0) @ K \_/ K') (Vptr (Ptr dfp 0) @ K \_/ K').
exact: indistxx.
move: (indist_registerUpdate_aux r3 indist_rs ind).
rewrite upd_r3 upd_r32 {1}/indist /= => ->; rewrite andbT.
have P: forall μ1 μ2 μ1' μ2' L dfp fr,
indistMemAsym obs μ1 μ2 ->
Mem.alloc Local μ1 L fr = (dfp,μ1') ->
Mem.alloc Local μ2 L fr = (dfp,μ2') ->
indistMemAsym obs μ1' μ2'.
move=> {μ μ' μ2 μ2' dfp Halloc Halloc2 wf_s1 wf_s2 indist_μ indist_s1s2 upd_r3 upd_r32 ind}.
move=> μ1 μ2 μ1' μ2' L dfp fr /allP ind H1 H2.
apply/allP=> b.
rewrite /blocks_stamped_below -Mem.get_blocks_spec /allThingsBelow mem_filter all_elems.
rewrite andbT (Mem.alloc_get_frame H1) => /andP [low_b].
rewrite (Mem.alloc_get_frame H2).
move: low_b; have [<-{b}|ne low_b get_b] := altP (dfp =P b); first by rewrite indistxx.
suff /(ind b): b \in blocks_stamped_below obs μ1 by [].
rewrite /blocks_stamped_below /allThingsBelow -Mem.get_blocks_spec.
by rewrite mem_filter low_b all_elems.
case/andP: indist_μ=> [ind1 ind2].
rewrite /indist /=.
by rewrite (P _ _ _ _ _ _ _ ind1 Halloc Halloc2) (P _ _ _ _ _ _ _ ind2 Halloc2 Halloc).
apply/andP; split; last first.
have indist_dfp: indist obs (Vptr (Ptr dfp 0) @ K \_/ K')
(Vptr (Ptr dfp2 0) @ K \_/ K').
by rewrite /indist /= eqxx /= flows_join (negbTE hi_K') andbF.
move: (indist_registerUpdate_aux r3 indist_rs indist_dfp).
by rewrite upd_r3 upd_r32.
have hiL: isHigh (K \_/ (K' \_/ LPC)) obs.
by rewrite !flows_join (negbTE hi_K') andbF.
case/andP: indist_μ => [ind1 ind2].
rewrite /indist /= (P1 _ _ _ _ _ _ _ _ _ _ ind1 hiL hiL Halloc Halloc2).
by rewrite (P1 _ _ _ _ _ _ _ _ _ _ ind2 hiL hiL Halloc2 Halloc).
have hiL: isHigh (K \_/ (K' \_/ LPC)) obs.
by rewrite flows_join (negbTE hi_K).
rewrite {1}/indist /=.
case/andP: indist_μ=> [ind1 ind2].
rewrite (P1 _ _ _ _ _ _ _ _ _ _ ind1 hiL hiL Halloc Halloc2).
rewrite (P1 _ _ _ _ _ _ _ _ _ _ ind2 hiL hiL Halloc2 Halloc) /=.
have indist_dfp: indist obs (Vptr (Ptr dfp 0) @ K \_/ K')
(Vptr (Ptr dfp2 0) @ K \_/ K').
by rewrite /indist /= eqxx /= flows_join (negbTE hi_K).
move: (indist_registerUpdate_aux r3 indist_rs indist_dfp).
by rewrite upd_r3 upd_r32.
(* Load *)
+ move=> im μ σ pc C [pv pl] K r r' r1 r2 j LPC v Ll rl rpcl -> /= CODE get_r1 load_p mlab_p [<- <-].
rewrite /Vector.nth_order /= => upd_r2 low_pc1 indist_s1s2 wf_s1.
rewrite /fstep -(indist_instr indist_s1s2) /state_instr_lookup //= CODE /=.
case: s2 wf_s2 indist_s1s2
=> [im2 μ2 σ2 rs2 [j2 LPC2]] //= wf_s2 indist_s1s2.
case get_r1': registerContent=> [[[|[pv' pl']|] K']|] //=.
have /= [a] := indist_registerContent indist_s1s2 low_pc1 get_r1.
rewrite get_r1' => - [<-] {a} /andP [/eqP eK indist_p]; subst K'.
case get_pv: (Mem.get_frame μ pv) load_p mlab_p => [[fl fr]|] //= load_p [eC].
subst fl.
case get_pv': Mem.get_frame=> [[C' fr']|] //=.
case load_p': nth_error_Z=> [[v' Ll']|] //=.
rewrite /Vector.nth_order /=.
case upd_r2': registerUpdate=> [rs2'|] //= [<-] {s2'}.
move: indist_s1s2 (indist_s1s2).
rewrite {1}indist_low_pc //= => /and5P [? ind_μ ? /eqP [? ?] ind_rs] indist_s1s2; subst j2 LPC2.
rewrite /indist /= !flows_join low_pc1 /=.
apply/and3P; split=> //.