-
Notifications
You must be signed in to change notification settings - Fork 0
/
Reordering.v
6216 lines (5966 loc) · 233 KB
/
Reordering.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 BinNat.
Require Import Bool.
Require Import List.
Require Import sflib.
Require Import Omega.
Require Import Common.
Require Import Lang.
Require Import Value.
Require Import Memory.
Require Import State.
Require Import LoadStore.
Require Import SmallStep.
Require Import SmallStepAux.
Require Import SmallStepWf.
Require Import Behaviors.
Module Ir.
Module Reordering.
(* Checks whether instruction i2 has data dependency on instruction i1.
There's no data dependency, reordering 'i1;i2' into 'i2;i1' wouldn't break use-def chain.
Note that this function does not check whether bi2 dominates i1.
If i1 has no def (e.g. store instruction), this returns false. *)
Definition has_data_dependency (i1 i2:Ir.Inst.t): bool :=
match (Ir.Inst.def i1) with
| None => false
| Some (r1, _) => (List.existsb (fun r => Nat.eqb r r1) (Ir.Inst.regops i2))
end.
(* Checks whether a program `i1;i2` is well-formed.
This checks four things:
(1) defs of i1 and i2 aren't the same (by SSA)
(2) i1's use never contains i2's def, because i1 is never phi-node by definition of Ir.Inst.
(Note that this is possible if i1;i2 is in a dead loop,
but for simplity I'll assume that there's no dead loop.)
(3) i2's use never contains i2's def, in the same reason, and
(4) i1's use never contains i1's def. *)
Definition program_wellformed (i1 i2:Ir.Inst.t): bool :=
match (Ir.Inst.def i2) with
| None =>
match Ir.Inst.def i1 with
| None => true
| Some (r1, _) =>
negb (List.existsb (fun r => Nat.eqb r r1) (Ir.Inst.regops i1))
end
| Some (r2, _) =>
match Ir.Inst.def i1 with
| None => true
| Some (r1, _) =>
(negb (Nat.eqb r1 r2))
&& (negb (List.existsb (fun r => Nat.eqb r r1) (Ir.Inst.regops i1)))
end
&& (negb (List.existsb (fun r => Nat.eqb r r2) (Ir.Inst.regops i1)))
&& (negb (List.existsb (fun r => Nat.eqb r r2) (Ir.Inst.regops i2)))
end.
(* Analogous to Ir.SmallStep.incrpc, except that it returns None if there's no
trivial next pc. *)
Definition incrpc' (md:Ir.IRModule.t) (c:Ir.Config.t):option Ir.Config.t :=
match (Ir.Config.cur_fdef_pc md c) with
| Some (fdef, pc0) =>
match (Ir.IRFunction.next_trivial_pc pc0 fdef) with
| Some pc' =>
Some (Ir.Config.update_pc c pc')
| None => None (* Cannot happen..! *)
end
| None => None (* Cannot happen *)
end.
(* This proposition holds iff current pc points to i1,
and the next pc points to i2. *)
Definition inst_locates_at (md:Ir.IRModule.t) (c:Ir.Config.t) (i1 i2:Ir.Inst.t):Prop :=
exists c',
Ir.Config.cur_inst md c = Some i1 /\
Some c' = incrpc' md c /\
Ir.Config.cur_inst md c' = Some i2.
(*****************************************************
Lemmas about various functions
*****************************************************)
Lemma incrpc'_incrpc:
forall md st st'
(HINCRPC':Some st' = incrpc' md st),
st' = Ir.SmallStep.incrpc md st.
Proof.
intros.
unfold incrpc' in *.
unfold Ir.SmallStep.incrpc.
des_ifs.
Qed.
Lemma inst_step_incrpc:
forall md st e st' st2'
(HINCR:Some st' = incrpc' md st)
(HSTEP:Ir.SmallStep.inst_step md st (Ir.SmallStep.sr_success e st2')),
Ir.Config.cur_inst md st' = Ir.Config.cur_inst md st2'.
Proof.
intros.
apply incrpc'_incrpc in HINCR.
inv HSTEP;
try (rewrite Ir.SmallStep.cur_inst_update_reg_and_incrpc; reflexivity).
- unfold Ir.SmallStep.inst_det_step in HNEXT.
des_ifs;
try(rewrite Ir.SmallStep.cur_inst_update_reg_and_incrpc; reflexivity);
try(rewrite Ir.SmallStep.incrpc_update_m; rewrite Ir.Config.cur_inst_update_m; reflexivity).
- rewrite Ir.SmallStep.cur_inst_update_reg_and_incrpc.
rewrite Ir.SmallStep.incrpc_update_m.
rewrite Ir.Config.cur_inst_update_m.
reflexivity.
Qed.
(****************************************
Lemmas about Ir.SmallStep.inst_step
****************************************)
(* If instruction i does not allocate memory, it does not raise OOM. *)
Lemma no_alloc_no_oom:
forall i st md
(HNOMEMCHG:Ir.SmallStep.allocates_mem i = false)
(HINST:Ir.Config.cur_inst md st = Some i)
(HOOM:Ir.SmallStep.inst_step md st Ir.SmallStep.sr_oom),
False.
Proof.
intros.
inversion HOOM.
- unfold Ir.SmallStep.inst_det_step in HNEXT.
rewrite HINST in HNEXT.
destruct i; des_ifs.
- rewrite HINST in HCUR.
inversion HCUR. rewrite HINST0 in H1.
rewrite <- H1 in HNOMEMCHG. inversion HNOMEMCHG.
Qed.
Lemma never_goes_wrong_no_gw:
forall i st md
(HNOMEMCHG:Ir.SmallStep.never_goes_wrong i = true)
(HINST:Ir.Config.cur_inst md st = Some i)
(HGW:Ir.SmallStep.inst_step md st Ir.SmallStep.sr_goes_wrong),
False.
Proof.
intros.
inv HGW.
unfold Ir.SmallStep.inst_det_step in HNEXT.
des_ifs.
Qed.
(* If instruction i does not finish program.
(note that ret is terminator) *)
Lemma inst_no_prog_finish:
forall i st md v
(HINST:Ir.Config.cur_inst md st = Some i)
(HOOM:Ir.SmallStep.inst_step md st (Ir.SmallStep.sr_prog_finish v)),
False.
Proof.
intros.
inversion HOOM.
- unfold Ir.SmallStep.inst_det_step in HNEXT.
rewrite HINST in HNEXT.
destruct i; des_ifs.
Qed.
(* If instruction i does not allocate memory, it either goes wrong
or succeed. *)
Lemma no_alloc_goes_wrong_or_success:
forall i st md sr
(HINST:Ir.Config.cur_inst md st = Some i)
(HNOALLOC:Ir.SmallStep.allocates_mem i = false)
(HNEXT:Ir.SmallStep.inst_step md st sr),
(sr = Ir.SmallStep.sr_goes_wrong \/
exists e st', sr = Ir.SmallStep.sr_success e st').
Proof.
intros.
inv HNEXT;
try (rewrite <- HCUR in HINST;
inv HINST; simpl in HNOALLOC; congruence);
try (right; eexists; eexists; reflexivity).
unfold Ir.SmallStep.inst_det_step in HNEXT0.
rewrite HINST in HNEXT0.
des_ifs;
try (left; reflexivity);
try (right; eexists; eexists; reflexivity).
Qed.
(***************************************************
Definition of equivalence of inst_nstep results
**************************************************)
Inductive nstep_eq: (Ir.trace * Ir.SmallStep.step_res) ->
(Ir.trace * Ir.SmallStep.step_res) -> Prop :=
| nseq_goes_wrong:
forall (t1 t2:Ir.trace)
(HEQ:List.filter Ir.not_none t1 = List.filter Ir.not_none t2),
nstep_eq (t1, (Ir.SmallStep.sr_goes_wrong)) (t2, (Ir.SmallStep.sr_goes_wrong))
| nseq_oom:
forall (t1 t2:Ir.trace)
(HEQ:List.filter Ir.not_none t1 = List.filter Ir.not_none t2),
nstep_eq (t1, (Ir.SmallStep.sr_oom)) (t2, (Ir.SmallStep.sr_oom))
| nseq_prog_finish:
forall (t1 t2:Ir.trace) v
(HEQ:List.filter Ir.not_none t1 = List.filter Ir.not_none t2),
nstep_eq (t1, (Ir.SmallStep.sr_prog_finish v)) (t2, (Ir.SmallStep.sr_prog_finish v))
| nseq_success:
forall (t1 t2:Ir.trace) e c1 c2
(HEQ:List.filter Ir.not_none t1 = List.filter Ir.not_none t2)
(HCEQ:Ir.Config.eq_wopc c1 c2),
nstep_eq (t1, (Ir.SmallStep.sr_success e c1))
(t2, (Ir.SmallStep.sr_success e c2)).
Lemma nstep_eq_refl:
forall sr, nstep_eq sr sr.
Proof.
destruct sr.
destruct s.
- constructor. reflexivity. apply Ir.Config.eq_wopc_refl.
- constructor. reflexivity.
- constructor. reflexivity.
- constructor. reflexivity.
Qed.
(* This lemma is valid because eq_wopc does not compare PCs. *)
Lemma nstep_eq_trans_1:
forall tr e md1 md2 sr' st r1 v1 r2 v2
(HNEQ:r1 <> r2),
nstep_eq (tr, Ir.SmallStep.sr_success e
(Ir.SmallStep.update_reg_and_incrpc md1 (Ir.SmallStep.update_reg_and_incrpc md1 st r1 v1) r2 v2))
sr'
<->
nstep_eq (tr, Ir.SmallStep.sr_success e
(Ir.SmallStep.update_reg_and_incrpc md2 (Ir.SmallStep.update_reg_and_incrpc md2 st r2 v2) r1 v1))
sr'.
Proof.
intros.
split.
{ intros HEQ.
inv HEQ.
constructor.
assumption.
assert (Ir.Config.eq_wopc
(Ir.SmallStep.update_reg_and_incrpc md2 (Ir.SmallStep.update_reg_and_incrpc md2 st r2 v2) r1 v1)
(Ir.SmallStep.update_reg_and_incrpc md1 (Ir.SmallStep.update_reg_and_incrpc md1 st r1 v1) r2 v2)).
{ apply Ir.SmallStep.eq_wopc_update_reg_and_incrpc_reorder. assumption. }
eapply Ir.Config.eq_wopc_trans.
eassumption.
eassumption.
}
{ intros HEQ.
inv HEQ.
constructor.
assumption.
assert (Ir.Config.eq_wopc
(Ir.SmallStep.update_reg_and_incrpc md1 (Ir.SmallStep.update_reg_and_incrpc md1 st r1 v1) r2 v2)
(Ir.SmallStep.update_reg_and_incrpc md2 (Ir.SmallStep.update_reg_and_incrpc md2 st r2 v2) r1 v1)).
{ apply Ir.SmallStep.eq_wopc_update_reg_and_incrpc_reorder.
apply not_eq_sym. assumption. }
eapply Ir.Config.eq_wopc_trans.
eassumption.
eassumption.
}
Qed.
(* This lemma is valid because eq_wopc does not compare PCs. *)
Lemma nstep_eq_trans_2:
forall tr e md1 md2 sr' st r1 v1 r2 v2 m
(HNEQ:r1 <> r2),
nstep_eq (tr, Ir.SmallStep.sr_success e
(Ir.SmallStep.update_reg_and_incrpc md1
(Ir.Config.update_m (Ir.SmallStep.update_reg_and_incrpc md1 st r1 v1) m) r2 v2)) sr'
<->
nstep_eq (tr, Ir.SmallStep.sr_success e
(Ir.SmallStep.update_reg_and_incrpc md2
(Ir.SmallStep.update_reg_and_incrpc md2 (Ir.Config.update_m st m) r2 v2) r1 v1))
sr'.
Proof.
intros.
split.
{ intros HEQ.
inv HEQ.
constructor.
assumption.
rewrite <- Ir.SmallStep.update_reg_and_incrpc_update_m in HCEQ.
assert (Ir.Config.eq_wopc
(Ir.SmallStep.update_reg_and_incrpc md2 (Ir.SmallStep.update_reg_and_incrpc md2 (Ir.Config.update_m st m) r2 v2) r1 v1)
(Ir.SmallStep.update_reg_and_incrpc md1 (Ir.SmallStep.update_reg_and_incrpc md1 (Ir.Config.update_m st m) r1 v1) r2 v2)).
{ eapply Ir.SmallStep.eq_wopc_update_reg_and_incrpc_reorder. assumption. }
eapply Ir.Config.eq_wopc_trans.
eassumption.
eassumption.
}
{ intros HEQ.
inv HEQ.
constructor.
assumption.
rewrite <- Ir.SmallStep.update_reg_and_incrpc_update_m.
assert (Ir.Config.eq_wopc
(Ir.SmallStep.update_reg_and_incrpc md2 (Ir.SmallStep.update_reg_and_incrpc md2 (Ir.Config.update_m st m) r2 v2) r1 v1)
(Ir.SmallStep.update_reg_and_incrpc md1 (Ir.SmallStep.update_reg_and_incrpc md1 (Ir.Config.update_m st m) r1 v1) r2 v2)).
{ eapply Ir.SmallStep.eq_wopc_update_reg_and_incrpc_reorder. assumption. }
apply Ir.Config.eq_wopc_symm in H.
eapply Ir.Config.eq_wopc_trans.
eassumption.
eassumption.
}
Qed.
Lemma nstep_eq_trans_3:
forall tr e md1 md2 sr' st r v m,
nstep_eq (tr, Ir.SmallStep.sr_success e
(Ir.SmallStep.update_reg_and_incrpc md1
(Ir.Config.update_m (Ir.SmallStep.incrpc md1 st) m) r v)) sr'
<->
nstep_eq (tr, Ir.SmallStep.sr_success e
(Ir.SmallStep.incrpc md2
(Ir.Config.update_m
(Ir.SmallStep.update_reg_and_incrpc md2 st r v) m))) sr'.
Proof.
intros.
split.
{ intros H.
inv H.
constructor.
assumption.
rewrite <- Ir.SmallStep.update_reg_and_incrpc_update_m.
rewrite Ir.SmallStep.incrpc_update_reg_and_incrpc.
rewrite Ir.SmallStep.incrpc_update_m.
apply Ir.Config.eq_wopc_trans with (c2 := (Ir.SmallStep.update_reg_and_incrpc md1
(Ir.Config.update_m (Ir.SmallStep.incrpc md1 st) m) r v));
try assumption.
unfold Ir.SmallStep.update_reg_and_incrpc.
apply Ir.SmallStep.config_eq_wopc_incrpc.
apply Ir.Config.eq_wopc_symm.
apply Ir.SmallStep.config_eq_wopc_incrpc.
apply Ir.Config.eq_wopc_update_rval.
apply Ir.Config.eq_wopc_update_m.
apply Ir.SmallStep.config_eq_wopc_incrpc.
apply Ir.Config.eq_wopc_symm.
apply Ir.SmallStep.config_eq_wopc_incrpc.
apply Ir.Config.eq_wopc_refl.
}
{ intros H.
inv H.
constructor.
assumption.
rewrite Ir.SmallStep.update_reg_and_incrpc_update_m.
rewrite <- Ir.SmallStep.incrpc_update_reg_and_incrpc.
rewrite <- Ir.SmallStep.incrpc_update_m.
apply Ir.Config.eq_wopc_trans with
(c2 := (Ir.SmallStep.incrpc md2
(Ir.Config.update_m (Ir.SmallStep.update_reg_and_incrpc md2 st r v) m)));
try assumption.
unfold Ir.SmallStep.update_reg_and_incrpc.
apply Ir.SmallStep.config_eq_wopc_incrpc.
apply Ir.Config.eq_wopc_symm.
apply Ir.SmallStep.config_eq_wopc_incrpc.
apply Ir.Config.eq_wopc_update_m.
apply Ir.SmallStep.config_eq_wopc_incrpc.
apply Ir.Config.eq_wopc_symm.
apply Ir.SmallStep.config_eq_wopc_incrpc.
apply Ir.Config.eq_wopc_update_rval.
apply Ir.Config.eq_wopc_refl.
}
Qed.
(***************************************************
Definition of valid reordering.
**************************************************)
(* Is it valid to reorder 'i1;i2' into 'i2;i1'? *)
Definition inst_reordering_valid (i1 i2:Ir.Inst.t): Prop :=
forall
(* If there's no data dependency from i1 to i2 *)
(HNODEP:has_data_dependency i1 i2 = false)
(HPROGWF:program_wellformed i1 i2 = true),
(* 'i1;i2' -> 'i2;i1' is allowed *)
forall (md md':Ir.IRModule.t) (* IR Modules *)
(sr:Ir.trace * Ir.SmallStep.step_res)
(st:Ir.Config.t) (* Initial state *)
(HWF:Ir.Config.wf md st) (* Well-formedness of st *)
(HLOCATE:inst_locates_at md st i1 i2)
(HLOCATE':inst_locates_at md' st i2 i1)
(HSTEP:Ir.SmallStep.inst_nstep md' st 2 sr),
exists sr', (* step result after 'i1;i2' *)
Ir.SmallStep.inst_nstep md st 2 sr' /\
nstep_eq sr sr'.
Ltac do_nseq_refl :=
apply nseq_success; try reflexivity; apply Ir.Config.eq_wopc_refl.
Ltac inv_cur_inst HCUR HLOCATE :=
rewrite HLOCATE in HCUR; inv HCUR.
Ltac inv_cur_inst_next HCUR HLOCATE2 HLOCATE_NEXT :=
apply incrpc'_incrpc in HLOCATE_NEXT; rewrite HLOCATE_NEXT in HLOCATE2;
try (rewrite Ir.SmallStep.incrpc_update_m in HCUR); try (rewrite Ir.Config.cur_inst_update_m in HCUR);
try (rewrite HLOCATE2 in HCUR); inv HCUR.
Ltac s_malloc_null_trivial HLOCATE2' :=
eapply Ir.SmallStep.s_malloc_null;
try (try (rewrite Ir.SmallStep.cur_inst_update_reg_and_incrpc);
rewrite HLOCATE2');
try reflexivity.
Ltac s_malloc_trivial HLOCATE2' :=
eapply Ir.SmallStep.s_malloc;
try (try rewrite Ir.SmallStep.m_update_reg_and_incrpc; eauto);
try (rewrite Ir.SmallStep.cur_inst_update_reg_and_incrpc; try rewrite HLOCATE2'; reflexivity).
Ltac inst_step_det_trivial HLOCATE' Hop1 Hop2 :=
apply Ir.SmallStep.s_det; unfold Ir.SmallStep.inst_det_step;
rewrite HLOCATE'; rewrite Hop1; try (rewrite Hop2); reflexivity.
Ltac inst_step_icmp_det_ptr_trivial HLOCATE' Hop1 Hop2 Heqptr :=
apply Ir.SmallStep.s_det; unfold Ir.SmallStep.inst_det_step;
rewrite HLOCATE'; rewrite Hop1; rewrite Hop2; rewrite Heqptr; reflexivity.
Ltac unfold_det HNEXT HLOCATE :=
unfold Ir.SmallStep.inst_det_step in HNEXT;
try rewrite Ir.SmallStep.cur_inst_update_reg_and_incrpc in HNEXT;
rewrite HLOCATE in HNEXT.
(********************************************
REORDERING of malloc - psub:
r1 = malloc ty opptr1
r2 = psub opty2 op21 op22
->
r2 = psub opty2 op21 op22
r1 = malloc ty opptr1.
**********************************************)
(* Lemma: Ir.SmallStep.p2N returns unchanged value even
if Memory.new is called *)
Lemma p2N_new_invariant:
forall md st op l0 o0 m' l blkty nsz a c P n0
(HWF:Ir.Config.wf md st)
(HGV: Ir.Config.get_val st op = Some (Ir.ptr (Ir.plog l0 o0)))
(HNEW:(m', l) = Ir.Memory.new (Ir.Config.m st) blkty nsz a c P)
(HDISJ:Ir.Memory.allocatable (Ir.Config.m st)
(List.map (fun addr => (addr, nsz)) P) = true)
(HSZ2:nsz > 0)
(HMBWF:forall begt, Ir.MemBlock.wf (Ir.MemBlock.mk (Ir.heap) (begt, None) nsz
(Ir.SYSALIGN) c P)),
Ir.SmallStep.p2N (Ir.plog l0 o0) (Ir.Config.m (Ir.Config.update_m st m')) n0 =
Ir.SmallStep.p2N (Ir.plog l0 o0) (Ir.Config.m st) n0.
Proof.
intros.
unfold Ir.SmallStep.p2N.
unfold Ir.log_to_phy.
destruct HWF.
dup HGV.
apply wf_ptr in HGV0.
assert (HL:l = Ir.Memory.fresh_bid (Ir.Config.m st)).
{ unfold Ir.Memory.new in HNEW. inv HNEW. reflexivity. }
erewrite Ir.Memory.get_new; try eassumption. reflexivity.
inv HGV0. exploit H. reflexivity. intros HH. inv HH.
inv H2.
eapply Ir.Memory.get_fresh_bid; eassumption.
Qed.
Lemma psub_always_succeeds:
forall st (md:Ir.IRModule.t) r retty ptrty op1 op2
(HCUR: Ir.Config.cur_inst md st = Some (Ir.Inst.ipsub r retty ptrty op1 op2)),
exists st' v,
(Ir.SmallStep.inst_step md st (Ir.SmallStep.sr_success Ir.e_none st') /\
(st' = Ir.SmallStep.update_reg_and_incrpc md st r v)).
Proof.
intros.
destruct (Ir.Config.get_val st op1) eqn:Hop1;
destruct (Ir.Config.get_val st op2) eqn:Hop2;
(eexists; eexists; split;
[ eapply Ir.SmallStep.s_det; unfold Ir.SmallStep.inst_det_step;
rewrite HCUR; rewrite Hop1; reflexivity
| reflexivity ]).
Qed.
Lemma psub_always_succeeds2:
forall st st' (md:Ir.IRModule.t) r retty ptrty op1 op2
(HCUR: Ir.Config.cur_inst md st = Some (Ir.Inst.ipsub r retty ptrty op1 op2))
(HSTEP: Ir.SmallStep.inst_step md st st'),
exists v, st' = Ir.SmallStep.sr_success Ir.e_none
(Ir.SmallStep.update_reg_and_incrpc md st r v).
Proof.
intros.
inv HSTEP; try congruence.
unfold Ir.SmallStep.inst_det_step in HNEXT.
rewrite HCUR in HNEXT.
destruct (Ir.Config.get_val st op1) eqn:Hop1;
destruct (Ir.Config.get_val st op2) eqn:Hop2;
try (des_ifs; eexists; reflexivity).
Qed.
Lemma psub_new_invariant:
forall md l m' (p1 p2:Ir.ptrval) st nsz contents P op1 op2 (sz:nat)
(HWF:Ir.Config.wf md st)
(HGV1: Ir.Config.get_val st op1 = Some (Ir.ptr p1))
(HGV2: Ir.Config.get_val st op2 = Some (Ir.ptr p2))
(HALLOC:Ir.Memory.allocatable (Ir.Config.m st) (map (fun addr : nat => (addr, nsz)) P) = true)
(HSZ:nsz > 0)
(HMBWF:forall begt, Ir.MemBlock.wf (Ir.MemBlock.mk (Ir.heap) (begt, None) nsz
(Ir.SYSALIGN) contents P))
(HNEW:(m', l) =
Ir.Memory.new (Ir.Config.m st) Ir.heap nsz Ir.SYSALIGN contents P),
Ir.SmallStep.psub p1 p2 (Ir.Config.m (Ir.Config.update_m st m')) sz =
Ir.SmallStep.psub p1 p2 (Ir.Config.m st) sz.
Proof.
intros.
unfold Ir.SmallStep.psub.
destruct p1.
{ destruct p2; try reflexivity.
erewrite p2N_new_invariant; try eassumption. reflexivity.
}
{ destruct p2.
{ erewrite p2N_new_invariant;try eassumption. reflexivity. }
reflexivity.
}
Qed.
Ltac dep_init HNODEP HINST1 HINST2 :=
unfold has_data_dependency in HNODEP; rewrite HINST1, HINST2 in HNODEP;
simpl in HNODEP.
Ltac pwf_init HPROGWF HINST1 HINST2 :=
unfold program_wellformed in HPROGWF; rewrite HINST1, HINST2 in HPROGWF;
simpl in HPROGWF.
Ltac solve_op_r op21 HH r1 :=
destruct op21 as [ | r]; try congruence; simpl in HH;
try repeat (rewrite orb_false_r in HH);
destruct (r =? r1) eqn:HR;
[ simpl in HH; try repeat (rewrite andb_false_r in HH);
inv HH; fail | apply beq_nat_false in HR; congruence ].
Lemma existsb_app2 {X:Type}:
forall (l1 l2:list X) (f:X -> bool),
existsb f (l1++l2) = existsb f (l2++l1).
Proof.
intros.
induction l1.
{ rewrite app_nil_r. ss. }
{ simpl. do 2 rewrite existsb_app. simpl.
do 2 rewrite orb_assoc. rewrite orb_comm.
rewrite orb_assoc. ss.
}
Qed.
Theorem reorder_malloc_psub:
forall i1 i2 r1 r2 (op21 op22 opptr1:Ir.op) retty2 ptrty2 ty1
(HINST1:i1 = Ir.Inst.imalloc r1 ty1 opptr1)
(HINST2:i2 = Ir.Inst.ipsub r2 retty2 ptrty2 op21 op22),
inst_reordering_valid i1 i2.
Proof.
intros.
unfold inst_reordering_valid.
intros.
assert (HOP21_NEQ_R1:op21 <> Ir.opreg r1).
{ dep_init HNODEP HINST1 HINST2.
solve_op_r op21 HNODEP r1. }
assert (HOP22_NEQ_R1:op22 <> Ir.opreg r1).
{ dep_init HNODEP HINST1 HINST2.
rewrite existsb_app2 in HNODEP.
solve_op_r op22 HNODEP r1. }
assert (HOPPTR1_NEQ_R1:opptr1 <> Ir.opreg r1).
{ pwf_init HPROGWF HINST1 HINST2.
solve_op_r opptr1 HPROGWF r1. }
assert (HOPPTR1_NEQ_R2:opptr1 <> Ir.opreg r2).
{ pwf_init HPROGWF HINST1 HINST2.
solve_op_r opptr1 HPROGWF r2. }
assert (HOP21_NEQ_R2:op21 <> Ir.opreg r2).
{ pwf_init HPROGWF HINST1 HINST2.
solve_op_r op21 HPROGWF r2. }
assert (HOP22_NEQ_R2:op22 <> Ir.opreg r2).
{ pwf_init HPROGWF HINST1 HINST2.
rewrite existsb_app2 in HPROGWF.
solve_op_r op22 HPROGWF r2. }
assert (HR1_NEQ_R2:r1 <> r2).
{ pwf_init HPROGWF HINST1 HINST2.
destruct (r1 =? r2) eqn:HR. inv HPROGWF. apply beq_nat_false in HR. congruence.
}
destruct HLOCATE as [st_next [HLOCATE1 [HLOCATE_NEXT HLOCATE2]]].
destruct HLOCATE' as [st_next' [HLOCATE1' [HLOCATE_NEXT' HLOCATE2']]].
inv HSTEP.
- (* psub - always succeed. :) *)
inv HSUCC; try (inv HSUCC0; fail).
assert (HCUR':Ir.Config.cur_inst md' c' = Ir.Config.cur_inst md' st_next').
{ symmetry. eapply inst_step_incrpc. eassumption.
eassumption. }
inv HSINGLE; try congruence.
+ unfold Ir.SmallStep.inst_det_step in HNEXT.
rewrite HCUR' in HNEXT. rewrite HLOCATE2' in HNEXT. inv HNEXT.
+ (* malloc returns null *)
rewrite HCUR' in HCUR. rewrite HLOCATE2' in HCUR. inv HCUR.
apply incrpc'_incrpc in HLOCATE_NEXT.
rewrite HLOCATE_NEXT in HLOCATE2.
inv HSINGLE0; try congruence.
{
unfold Ir.SmallStep.inst_det_step in HNEXT.
rewrite HLOCATE1' in HNEXT. inv HNEXT.
des_ifs;
try (eexists; split;
[ eapply Ir.SmallStep.ns_success;
[ eapply Ir.SmallStep.ns_one;
s_malloc_null_trivial HLOCATE1
| eapply Ir.SmallStep.s_det;
unfold Ir.SmallStep.inst_det_step;
rewrite Ir.SmallStep.cur_inst_update_reg_and_incrpc;
rewrite HLOCATE2;
try (rewrite Ir.SmallStep.get_val_independent2;
[ rewrite Heq; reflexivity | assumption ]);
try reflexivity
]
| rewrite nstep_eq_trans_1;
[ apply nstep_eq_refl | congruence ] ]
).
all: try
(
eexists; split;
[ eapply Ir.SmallStep.ns_success;
[ eapply Ir.SmallStep.ns_one;
s_malloc_null_trivial HLOCATE1
| eapply Ir.SmallStep.s_det;
unfold Ir.SmallStep.inst_det_step;
rewrite Ir.SmallStep.cur_inst_update_reg_and_incrpc;
rewrite HLOCATE2;
rewrite Ir.SmallStep.get_val_independent2;
[ rewrite Heq; reflexivity | assumption ]
]
| try rewrite Ir.SmallStep.m_update_reg_and_incrpc;
rewrite Ir.SmallStep.get_val_independent2;
[ rewrite Heq0;
rewrite nstep_eq_trans_1;
[ apply nstep_eq_refl | congruence ]
| congruence ]
]
).
}
+ (* oom *)
rewrite HCUR' in HCUR. rewrite HLOCATE2' in HCUR. inv HCUR.
apply psub_always_succeeds2 with (r := r2) (retty := retty2)
(ptrty := ptrty2)
(op1 := op21) (op2 := op22) in HSINGLE0.
destruct HSINGLE0 as [vtmp HSINGLE0]. inv HSINGLE0.
eexists (nil, Ir.SmallStep.sr_oom).
split.
{ eapply Ir.SmallStep.ns_oom.
eapply Ir.SmallStep.ns_one.
eapply Ir.SmallStep.s_malloc_oom.
rewrite HLOCATE1. ss. ss.
rewrite Ir.SmallStep.get_val_independent2 in HSZ; eassumption.
rewrite Ir.SmallStep.m_update_reg_and_incrpc in HNOSPACE.
assumption.
}
{ constructor. reflexivity. }
assumption.
+ (* malloc succeeds *)
rewrite HCUR' in HCUR. rewrite HLOCATE2' in HCUR. inv HCUR.
apply incrpc'_incrpc in HLOCATE_NEXT.
rewrite HLOCATE_NEXT in HLOCATE2.
inv HSINGLE0; try congruence.
{ (* psub is determinsitic *)
unfold Ir.SmallStep.inst_det_step in HNEXT.
rewrite HLOCATE1' in HNEXT.
des_ifs;
rewrite Ir.SmallStep.m_update_reg_and_incrpc in *;
rewrite Ir.SmallStep.cur_inst_update_reg_and_incrpc in *.
all: try (eexists; split;
[ eapply Ir.SmallStep.ns_success;
[ (* malloc *)
eapply Ir.SmallStep.ns_one;
eapply Ir.SmallStep.s_malloc; try (eauto; fail);
rewrite Ir.SmallStep.get_val_independent2 in HSZ;
[ eassumption | congruence ]
| (* psub, det *)
eapply Ir.SmallStep.s_det;
unfold Ir.SmallStep.inst_det_step;
rewrite Ir.SmallStep.cur_inst_update_reg_and_incrpc;
rewrite Ir.SmallStep.cur_inst_incrpc_update_m;
rewrite HLOCATE2;
rewrite Ir.SmallStep.get_val_independent2;
[ reflexivity | congruence ]
]
| eapply nstep_eq_trans_2; try congruence;
rewrite Ir.Config.get_val_update_m;
rewrite Heq; try apply nstep_eq_refl;
try (rewrite Ir.SmallStep.get_val_independent2;
[ rewrite Ir.Config.get_val_update_m;
rewrite Heq0; apply nstep_eq_refl
| congruence ])
]
; fail).
{ (* psub deterministic *)
eexists. split.
{ eapply Ir.SmallStep.ns_success.
{ eapply Ir.SmallStep.ns_one.
s_malloc_trivial HLOCATE1'.
rewrite Ir.SmallStep.get_val_independent2 in HSZ; eauto.
}
{ eapply Ir.SmallStep.s_det.
unfold Ir.SmallStep.inst_det_step.
rewrite Ir.SmallStep.cur_inst_update_reg_and_incrpc.
rewrite Ir.SmallStep.cur_inst_incrpc_update_m.
rewrite HLOCATE2.
rewrite Ir.SmallStep.get_val_independent2; try eassumption.
rewrite Ir.Config.get_val_update_m, Heq.
rewrite Ir.SmallStep.get_val_independent2; try eassumption.
rewrite Ir.Config.get_val_update_m, Heq0.
rewrite Ir.SmallStep.m_update_reg_and_incrpc.
rewrite Ir.Config.m_update_m.
assert (HPTR:Ir.SmallStep.psub p p0 m' n =
Ir.SmallStep.psub p p0 (Ir.Config.m st) n).
{ erewrite <- psub_new_invariant; eauto.
rewrite Ir.Config.m_update_m. reflexivity. }
rewrite HPTR. reflexivity.
}
}
{
rewrite nstep_eq_trans_2.
{ apply nstep_eq_refl. }
{ congruence. }
}
}
{ (* psub deterministic *)
eexists. split.
{ eapply Ir.SmallStep.ns_success.
{ eapply Ir.SmallStep.ns_one.
s_malloc_trivial HLOCATE1'.
rewrite Ir.SmallStep.get_val_independent2 in HSZ; eassumption.
}
{ eapply Ir.SmallStep.s_det.
unfold Ir.SmallStep.inst_det_step.
rewrite Ir.SmallStep.cur_inst_update_reg_and_incrpc.
rewrite Ir.SmallStep.cur_inst_incrpc_update_m.
rewrite HLOCATE2.
reflexivity.
}
}
{
rewrite nstep_eq_trans_2.
{ apply nstep_eq_refl. }
{ congruence. }
}
}
}
- (* psub never raises OOM. *)
inv HOOM.
+ exfalso. exploit (no_alloc_no_oom (Ir.Inst.ipsub r2 retty2 ptrty2 op21 op22)).
reflexivity. eapply HLOCATE1'. eassumption. intros. assumption.
+ inv HSUCC.
+ inv HOOM0.
- (* psub never goes wrong. *)
inv HGW.
+ exfalso. exploit (never_goes_wrong_no_gw
(Ir.Inst.ipsub r2 retty2 ptrty2 op21 op22)).
reflexivity. eapply HLOCATE1'. assumption. intros. assumption.
+ inv HSUCC.
+ inv HGW0.
Qed.
(********************************************
REORDERING of psub - malloc:
r1 = psub retty1 ptrty1 op11 op12
r2 = malloc ty2 opptr2
->
r2 = malloc ty2 opptr2
r1 = psub retty1 ptrty1 op11 op12
**********************************************)
Theorem reorder_psub_malloc:
forall i1 i2 r1 r2 (opptr2 op11 op12:Ir.op) ty2 retty1 ptrty1
(HINST1:i1 = Ir.Inst.ipsub r1 retty1 ptrty1 op11 op12)
(HINST2:i2 = Ir.Inst.imalloc r2 ty2 opptr2),
inst_reordering_valid i1 i2.
Proof.
intros.
unfold inst_reordering_valid.
intros.
assert (HOP11_NEQ_R1:op11 <> Ir.opreg r1).
{ pwf_init HPROGWF HINST1 HINST2.
solve_op_r op11 HPROGWF r1. }
assert (HOP12_NEQ_R1:op12 <> Ir.opreg r1).
{ pwf_init HPROGWF HINST1 HINST2.
rewrite existsb_app2 in HPROGWF.
solve_op_r op12 HPROGWF r1. }
assert (HOPPTR2_NEQ_R1:opptr2 <> Ir.opreg r1).
{ dep_init HNODEP HINST1 HINST2.
solve_op_r opptr2 HNODEP r1. }
assert (HOPPTR2_NEQ_R2:opptr2 <> Ir.opreg r2).
{ pwf_init HPROGWF HINST1 HINST2.
solve_op_r opptr2 HPROGWF r2. }
assert (HOP11_NEQ_R2:op11 <> Ir.opreg r2).
{ pwf_init HPROGWF HINST1 HINST2.
solve_op_r op11 HPROGWF r2. }
assert (HOP12_NEQ_R2:op12 <> Ir.opreg r2).
{ pwf_init HPROGWF HINST1 HINST2.
rewrite existsb_app2 with (f := (fun r : nat => r =? r2)) in HPROGWF.
solve_op_r op12 HPROGWF r2. }
assert (HR1_NEQ_R2:r1 <> r2).
{ pwf_init HPROGWF HINST1 HINST2.
destruct (r1 =? r2) eqn:HR. inv HPROGWF. apply beq_nat_false in HR. congruence.
}
destruct HLOCATE as [st_next [HLOCATE1 [HLOCATE_NEXT HLOCATE2]]].
destruct HLOCATE' as [st_next' [HLOCATE1' [HLOCATE_NEXT' HLOCATE2']]].
(* HSTEP: 2 steps in target *)
inv HSTEP.
- (* malloc succeeds. *)
inv HSUCC; try (inv HSUCC0; fail).
(* HSUCC: the first step in target *)
exploit inst_step_incrpc. eapply HLOCATE_NEXT'. eapply HSINGLE0.
intros HCUR'.
inv HSINGLE; try congruence. (* HSINGLE: the second step in target *)
(* psub works deterministically. *)
(* HNEXT: Some sr0 = Ir.SmallStep.inst_det_step md' c' *)
unfold Ir.SmallStep.inst_det_step in HNEXT. rewrite <- HCUR' in HNEXT.
rewrite HLOCATE2' in HNEXT.
apply incrpc'_incrpc in HLOCATE_NEXT.
rewrite HLOCATE_NEXT in HLOCATE2.
(* now get malloc's behavior in the target*)
inv HSINGLE0; try congruence.
+ unfold Ir.SmallStep.inst_det_step in HNEXT0. rewrite HLOCATE1' in HNEXT0.
congruence.
+ (* Malloc returned NULL. *)
inv_cur_inst HCUR HLOCATE1'.
rewrite Ir.SmallStep.get_val_independent2 in HNEXT.
rewrite Ir.SmallStep.get_val_independent2 in HNEXT.
{
rewrite Ir.SmallStep.m_update_reg_and_incrpc in HNEXT.
destruct (Ir.Config.get_val st op11) eqn:Hop11;
destruct (Ir.Config.get_val st op12) eqn:Hop12.
{
destruct v; destruct v0; try inv HNEXT;
try (eexists; split;
[ eapply Ir.SmallStep.ns_success;
[ eapply Ir.SmallStep.ns_one;
inst_step_det_trivial HLOCATE1 Hop11 Hop12
| s_malloc_null_trivial HLOCATE2 ]
| eapply nstep_eq_trans_1;
[ congruence | apply nstep_eq_refl ]
]
).
}
{
destruct v; try inv HNEXT; try (
eexists; split;
[ eapply Ir.SmallStep.ns_success; [ eapply Ir.SmallStep.ns_one;
inst_step_det_trivial HLOCATE1 Hop11 Hop12 |
s_malloc_null_trivial HLOCATE2 ]
| eapply nstep_eq_trans_1;
[ congruence | apply nstep_eq_refl ]
]
).
}
{ inv HNEXT; try (
eexists; split;
[ eapply Ir.SmallStep.ns_success; [ eapply Ir.SmallStep.ns_one;
inst_step_det_trivial HLOCATE1 Hop11 Hop12 |
s_malloc_null_trivial HLOCATE2 ]
| eapply nstep_eq_trans_1;
[ congruence | apply nstep_eq_refl ] ]).
}
{ inv HNEXT; try (
eexists; split;
[ eapply Ir.SmallStep.ns_success; [ eapply Ir.SmallStep.ns_one;
inst_step_det_trivial HLOCATE1 Hop11 Hop12 |
s_malloc_null_trivial HLOCATE2 ]
| eapply nstep_eq_trans_1;
[ congruence | apply nstep_eq_refl ] ]).
}
}
{ congruence. }
{ congruence. }
+ (* malloc succeeded. *)
rewrite Ir.SmallStep.get_val_independent2 in HNEXT.
rewrite Ir.SmallStep.get_val_independent2 in HNEXT.
{
inv_cur_inst HCUR HLOCATE1'.
repeat (rewrite Ir.Config.get_val_update_m in HNEXT).
rewrite Ir.SmallStep.m_update_reg_and_incrpc in HNEXT.
des_ifs; try(
eexists; split;
[ eapply Ir.SmallStep.ns_success;
[ apply Ir.SmallStep.ns_one;
try (inst_step_det_trivial HLOCATE1 Heq Heq0; fail);
try (apply Ir.SmallStep.s_det; unfold Ir.SmallStep.inst_det_step;
rewrite HLOCATE1; reflexivity)
| s_malloc_trivial HLOCATE2;
rewrite Ir.SmallStep.get_val_independent2;
[ eassumption | congruence ]
]
| eapply nstep_eq_trans_2;
[ congruence | apply nstep_eq_refl ]
]
).
{ eexists. split.
{ eapply Ir.SmallStep.ns_success.
- apply Ir.SmallStep.ns_one.
apply Ir.SmallStep.s_det. unfold Ir.SmallStep.inst_det_step.
rewrite HLOCATE1. rewrite Heq. rewrite Heq0.
reflexivity.
- s_malloc_trivial HLOCATE2.
rewrite Ir.SmallStep.get_val_independent2. eassumption.
congruence.
}
{ eapply nstep_eq_trans_2.
{ congruence. }
{ assert (HPSUB:Ir.SmallStep.psub p p0 m' n =
Ir.SmallStep.psub p p0 (Ir.Config.m st) n).
{ erewrite <- psub_new_invariant; eauto. rewrite Ir.Config.m_update_m.
reflexivity. }
rewrite HPSUB. apply nstep_eq_refl. }
}
}
}
{ rewrite HLOCATE1' in HCUR. inv HCUR.
congruence.
}
{ rewrite HLOCATE1' in HCUR. inv HCUR.
congruence.
}
- (* malloc raised oom. *)
inv HOOM.
+ inv HSINGLE. unfold Ir.SmallStep.inst_det_step in HNEXT.
rewrite HLOCATE1' in HNEXT. inv HNEXT.
inv_cur_inst HCUR HLOCATE1'.
(* psub only succeeds. *)
assert (HSUCC := psub_always_succeeds st md r1 retty1 ptrty1
op11 op12 HLOCATE1).
destruct HSUCC as [st'tmp [v'tmp [HSUCC1 HSUCC2]]].
eexists. split.
{ eapply Ir.SmallStep.ns_success.
- eapply Ir.SmallStep.ns_one.
eapply HSUCC1.
- eapply Ir.SmallStep.s_malloc_oom.
rewrite HSUCC2. apply incrpc'_incrpc in HLOCATE_NEXT.
rewrite HLOCATE_NEXT in HLOCATE2.
rewrite Ir.SmallStep.cur_inst_update_reg_and_incrpc. rewrite HLOCATE2.
reflexivity.
reflexivity.
rewrite HSUCC2.
rewrite Ir.SmallStep.get_val_independent2. eassumption.
congruence.
rewrite HSUCC2. rewrite Ir.SmallStep.m_update_reg_and_incrpc. eassumption.
}
{ constructor. reflexivity. }
+ inv HSUCC.
+ inv HOOM0.
- (* malloc never goes wrong. *)
inv HGW.
+ exfalso. exploit (never_goes_wrong_no_gw (Ir.Inst.imalloc r2 ty2 opptr2)).
reflexivity. eapply HLOCATE1'. eassumption.
intros. assumption.
+ inv HSUCC.
+ inv HGW0.
Qed.
(********************************************
REORDERING of free - psub:
free opptr1
r2 = psub retty2 ptrty2 op21 op22
->
r2 = psub retty2 ptrty2 op21 op22
free opptr1
**********************************************)
(* Lemma: Ir.SmallStep.p2N returns unchanged value even
if Memory.free is called *)
Lemma p2N_free_invariant:
forall md st op l0 o0 m' l n0
(HWF:Ir.Config.wf md st)
(HGV: Ir.Config.get_val st op = Some (Ir.ptr (Ir.plog l0 o0)))
(HFREE:Some m' = Ir.Memory.free (Ir.Config.m st) l),
Ir.SmallStep.p2N (Ir.plog l0 o0) m' n0 =
Ir.SmallStep.p2N (Ir.plog l0 o0) (Ir.Config.m st) n0.
Proof.
intros.
unfold Ir.SmallStep.p2N.
unfold Ir.log_to_phy.
destruct (Ir.Memory.get m' l0) eqn:Hget';
destruct (Ir.Memory.get (Ir.Config.m st) l0) eqn:Hget; try reflexivity.
{ rewrite Ir.Memory.get_free with (m := Ir.Config.m st) (m' := m')