-
Notifications
You must be signed in to change notification settings - Fork 0
/
myGraph.thy
810 lines (739 loc) · 35.9 KB
/
myGraph.thy
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
(* uses Isabelle2017 and autocorres version 1.0 *)
theory myGraph
imports
"checker-verification/Library/Autocorres_Misc"
"checker-verification/Witness_Property/Connected_Components"
"checker-verification/Witness_Property/ShortestPath"
begin
(* Parse the input file. *)
install_C_file "Graph_copy.c"
autocorres "Graph_copy.c"
context Graph_copy begin
thm "is_wellformed_body_def"
thm "trian_body_def"
thm "just_body_def"
thm "no_path_body_def"
thm "pos_cost_body_def"
thm "check_basic_just_sp_body_def"
thm "check_sp_body_def"
thm "is_wellformed'_def"
thm "trian'_def"
thm "just'_def"
thm "no_path'_def"
thm "pos_cost'_def"
thm "check_basic_just_sp'_def"
thm "check_sp'_def"
(*Implementation Graph Types*)
type_synonym IVertex = "32 word"
type_synonym IEdge_Id = "32 word"
type_synonym IEdge = "IVertex \<times> IVertex"
type_synonym IPEdge = "IVertex \<Rightarrow> 32 word"
type_synonym INum = "IVertex \<Rightarrow> 32 word"
type_synonym IDist = "IVertex \<Rightarrow> 32 word"
type_synonym ICost = "IVertex \<Rightarrow> 32 word"
type_synonym IGraph = "32 word \<times> 32 word \<times> (IEdge_Id \<Rightarrow> IEdge)"
abbreviation
ivertex_cnt :: "IGraph \<Rightarrow> 32 word"
where
"ivertex_cnt G \<equiv> fst G"
abbreviation
iedge_cnt :: "IGraph \<Rightarrow> 32 word"
where
"iedge_cnt G \<equiv> fst (snd G)"
abbreviation
iedges :: "IGraph \<Rightarrow> IEdge_Id \<Rightarrow> IEdge"
where
"iedges G \<equiv> snd (snd G)"
(* Make List - makes a list containing the result of a function *)
fun
bool::"32 word \<Rightarrow> bool"
where
"bool b = (if b=0 then False else True)"
fun
mk_list' :: "nat \<Rightarrow> (32 word \<Rightarrow> 'b) \<Rightarrow> 'b list"
where
"mk_list' n f = map f (map of_nat [0..<n])"
fun
mk_list'_temp :: "nat \<Rightarrow> (32 word \<Rightarrow> 'b) \<Rightarrow> nat \<Rightarrow> 'b list"
where
"mk_list'_temp 0 _ _ = []" |
"mk_list'_temp (Suc x) f i = (f (of_nat i)) # mk_list'_temp x f (Suc i)"
(* Make graph lists *)
fun
mk_iedge_list :: "IGraph \<Rightarrow> IEdge list"
where
"mk_iedge_list G = mk_list' (unat (iedge_cnt G)) (iedges G)"
fun
mk_inum_list :: "IGraph \<Rightarrow> INum \<Rightarrow> 32 word list"
where
"mk_inum_list G num = mk_list' (unat (ivertex_cnt G)) num"
fun
mk_ipedge_list :: "IGraph \<Rightarrow> IPEdge \<Rightarrow> 32 word list"
where
"mk_ipedge_list G pedge = mk_list' (unat (ivertex_cnt G)) pedge"
fun
mk_idist_list :: "IGraph \<Rightarrow> IDist \<Rightarrow> 32 word list"
where
"mk_idist_list G dis = mk_list' (unat (ivertex_cnt G)) dis"
fun
mk_icost_list :: "IGraph \<Rightarrow> ICost \<Rightarrow> 32 word list"
where
"mk_icost_list G cost = mk_list' (unat (iedge_cnt G)) cost"
(* Equate to Implementation *)
lemma sint_ucast:
"sint (ucast (x ::word32) :: sword32) = sint x"
by (clarsimp simp: sint_uint uint_up_ucast is_up)
fun
to_edge :: "IEdge \<Rightarrow> IEdge_C"
where
"to_edge (u,v) = IEdge_C u v"
lemma s_C_pte[simp]:
"first_C (to_edge e) = fst e"
by (cases e) auto
lemma t_C_pte[simp]:
"second_C (to_edge e) = snd e"
by (cases e) auto
definition is_graph where
"is_graph h iG p \<equiv>
is_valid_IGraph_C h p \<and>
ivertex_cnt iG = num_vertices_C (heap_IGraph_C h p) \<and>
iedge_cnt iG = num_edges_C (heap_IGraph_C h p) \<and>
arrlist (heap_IEdge_C h) (is_valid_IEdge_C h)
(map to_edge (mk_iedge_list iG)) (arcs_C (heap_IGraph_C h p))"
definition
"is_numm h iG iN (p:: 32 signed word ptr) \<equiv> arrlist (\<lambda>p. heap_w32 h (ptr_coerce p))
(\<lambda>p. is_valid_w32 h (ptr_coerce p)) (mk_inum_list iG iN) p"
definition
"is_pedge h iG iP (p:: 32 signed word ptr) \<equiv> arrlist (\<lambda>p. heap_w32 h (ptr_coerce p))
(\<lambda>p. is_valid_w32 h (ptr_coerce p)) (mk_ipedge_list iG iP) p"
definition
"is_dist h iG iD (p:: 32 signed word ptr) \<equiv> arrlist (\<lambda>p. heap_w32 h (ptr_coerce p))
(\<lambda>p. is_valid_w32 h (ptr_coerce p)) (mk_idist_list iG iD) p"
definition
"is_cost h iG iC p \<equiv> arrlist (heap_w32 h) (is_valid_w32 h) (mk_icost_list iG iC) p"
(* Abstract Graph *)
definition
no_loops :: "('a, 'b) pre_digraph \<Rightarrow> bool"
where
"no_loops G \<equiv> \<forall>e \<in> arcs G. tail G e \<noteq> head G e"
definition
abs_IGraph :: "IGraph \<Rightarrow> (32 word, 32 word) pre_digraph"
where
"abs_IGraph G \<equiv> \<lparr> verts = {0..<ivertex_cnt G}, arcs = {0..<iedge_cnt G},
tail = fst o iedges G, head = snd o iedges G \<rparr>"
lemma verts_absI[simp]: "verts (abs_IGraph G) = {0..<ivertex_cnt G}"
and edges_absI[simp]: "arcs (abs_IGraph G) = {0..<iedge_cnt G}"
and start_absI[simp]: "tail (abs_IGraph G) e = fst (iedges G e)"
and target_absI[simp]: "head (abs_IGraph G) e = snd (iedges G e)"
by (auto simp: abs_IGraph_def)
definition
abs_pedge :: "(32 word \<Rightarrow> 32 word) \<Rightarrow> 32 word \<Rightarrow> 32 word option"
where
"abs_pedge p \<equiv> (\<lambda>v. if sint (p v) < 0 then None else Some (p v))"
lemma None_abs_pedgeI[simp]:
"((abs_pedge p) v = None) = (sint (p v) < 0)"
using abs_pedge_def by auto
lemma Some_abs_pedgeI[simp]:
"(\<exists>e. (abs_pedge p) v = Some e) = (sint (p v) \<ge> 0)"
using None_not_eq None_abs_pedgeI
by (metis abs_pedge_def linorder_not_le option.simps(3))
(*Helper Lemmas*)
lemma wellformed_iGraph:
assumes "wf_digraph (abs_IGraph G)"
shows "\<And>e. e < iedge_cnt G \<Longrightarrow>
fst (iedges G e) < ivertex_cnt G \<and>
snd (iedges G e) < ivertex_cnt G"
using assms unfolding wf_digraph_def by simp
lemma unat_image_upto:
fixes n :: "32 word"
shows "unat ` {0..<n} = {unat 0..<unat n}" (is "?A = ?B")
proof
show "?B \<subseteq> ?A"
proof
fix i assume a: "i \<in> ?B"
then obtain i':: "32 word" where ii: "i= unat i'"
by (metis atLeastLessThan_iff le_unat_uoi less_or_eq_imp_le)
then have "i' \<in> {0..<n}"
using a word_less_nat_alt by auto
thus "i \<in> ?A" using ii by fast
qed
next
show "?A \<subseteq> ?B"
proof
fix i assume a: "i \<in> ?A"
then obtain i':: "32 word" where ii: "i= unat i'" by blast
then have "i' \<in> {0..<n}" using a by force
thus "i \<in> ?B"
by (metis Un_iff atLeast0LessThan ii ivl_disj_un(8)
lessThan_iff unat_0 unat_mono word_zero_le)
qed
qed
lemma path_length:
assumes "vpath p (abs_IGraph iG)"
shows "vwalk_length p < unat (ivertex_cnt iG)"
proof -
have pne: "p \<noteq> []" and dp: "distinct p" using assms by fast+
have "unat (ivertex_cnt iG) = card (unat ` {0..<(fst iG)})"
using unat_image_upto by simp
then have "unat (ivertex_cnt iG) = card ((verts (abs_IGraph iG)))"
by (simp add: inj_on_def card_image)
hence "length p \<le> unat (ivertex_cnt iG)"
by (metis finite_code card_mono vwalk_def
distinct_card[OF dp] vpath_def assms)
hence "length p - 1 < unat (ivertex_cnt iG)"
by (metis pne Nat.diff_le_self le_neq_implies_less
less_imp_diff_less minus_eq one_neq_zero length_0_conv)
thus "vwalk_length p < unat (fst iG)"
using assms
unfolding vpath_def vwalk_def by simp
qed
lemma ptr_coerce_ptr_add_uint[simp]:
"ptr_coerce (p +\<^sub>p uint x) = p +\<^sub>p (uint x)"
by auto
lemma pedge_num_dist_heap:
"\<lbrakk>arrlist (\<lambda>p. heap_w32 h p) (\<lambda>p. is_valid_w32 h p)
(map (iL \<circ> of_nat) [0..<unat n]) l; i < n\<rbrakk> \<Longrightarrow>
iL i = heap_w32 h (l +\<^sub>p int (unat i))"
apply (subgoal_tac
"heap_w32 h (l +\<^sub>p int (unat i)) = map (iL \<circ> of_nat) [0..<unat n] ! unat i")
apply (subgoal_tac "map (iL \<circ> of_nat) [0..<unat n] ! unat i = iL i")
apply fastforce
apply (metis (hide_lams, mono_tags) unat_mono word_unat.Rep_inverse
minus_nat.diff_0 nth_map_upt o_apply plus_nat.add_0)
apply (simp add: arrlist_nth_value unat_mono)
done
lemma pedge_num_dist_heap_ptr_coerce:
"\<lbrakk>arrlist (\<lambda>p. heap_w32 h (ptr_coerce p)) (\<lambda>p. is_valid_w32 h (ptr_coerce p))
(map (iL \<circ> of_nat) [0..<unat n]) l; i < n; 0 \<le> i\<rbrakk> \<Longrightarrow>
iL i = heap_w32 h (ptr_coerce (l +\<^sub>p int (unat i)))"
apply (subgoal_tac
"heap_w32 h (ptr_coerce (l +\<^sub>p int (unat i))) = map (iL \<circ> of_nat) [0..<unat n] ! unat i")
apply (subgoal_tac "map (iL \<circ> of_nat) [0..<unat n] ! unat i = iL i")
apply fastforce
apply (metis (hide_lams, mono_tags) unat_mono word_unat.Rep_inverse
minus_nat.diff_0 nth_map_upt o_apply plus_nat.add_0)
apply (drule arrlist_nth_value[where i="int (unat i)"], (simp add:unat_mono)+)
done
lemma edge_heap:
"\<lbrakk> arrlist h v (map (to_edge \<circ> (iedges iG \<circ> of_nat)) [0..<unat m]) ep;
e < m\<rbrakk> \<Longrightarrow> to_edge ((iedges iG) e) = h (ep +\<^sub>p (int (unat e)))"
apply (subgoal_tac "h (ep +\<^sub>p (int (unat e))) =
(map (to_edge \<circ> (iedges iG \<circ> of_nat)) [0..<unat m]) ! unat e")
apply (subgoal_tac "to_edge ((iedges iG) e) =
(map (to_edge \<circ> (iedges iG \<circ> of_nat)) [0..<unat m]) ! unat e")
apply presburger
apply (metis (hide_lams, mono_tags) length_map length_upt o_apply
map_upt_eq_vals_D minus_nat.diff_0 unat_mono word_unat.Rep_inverse)
apply (fastforce simp: unat_mono arrlist_nth_value)
done
lemma head_heap:
"\<lbrakk>arrlist h v (map (to_edge \<circ> (iedges iG \<circ> of_nat)) [0..<unat m]) ep; e < m\<rbrakk> \<Longrightarrow>
snd ((iedges iG) e) = second_C (h (ep +\<^sub>p (uint e)))"
using edge_heap to_edge.simps t_C_pte by (metis uint_nat)
lemma tail_heap:
"\<lbrakk>arrlist h v (map (to_edge \<circ> (iedges iG \<circ> of_nat)) [0..<unat m]) ep; e < m\<rbrakk> \<Longrightarrow>
fst ((iedges iG) e) = first_C (h (ep +\<^sub>p (uint e)))"
using edge_heap to_edge.simps s_C_pte uint_nat by metis
thm "is_wellformed'_def"
definition is_wellformed_inv :: "IGraph \<Rightarrow> 32 word \<Rightarrow> bool" where
"is_wellformed_inv G i \<equiv> \<forall>k < i. ivertex_cnt G > fst (iedges G k)
\<and> ivertex_cnt G > snd (iedges G k)"
lemma is_wellformed_spc':
"\<lbrace> P and
(\<lambda>s. wf_digraph (abs_IGraph iG) \<and>
is_graph s iG g) \<rbrace>
is_wellformed' g
\<lbrace> (\<lambda>_ s. P s) And
(\<lambda>rr s. rr \<noteq> 0 \<longleftrightarrow> is_wellformed_inv iG (iedge_cnt iG)) \<rbrace>!"
apply (clarsimp simp: is_wellformed'_def)
apply (subst whileLoopE_add_inv [where
M="\<lambda>(ee, s). unat (iedge_cnt iG - ee)" and
I="\<lambda>ee s. P s \<and> is_wellformed_inv iG ee \<and>
ee \<le> iedge_cnt iG \<and>
wf_digraph (abs_IGraph iG) \<and>
is_graph s iG g"])
apply (simp add: skipE_def)
apply wp
unfolding is_graph_def is_wellformed_inv_def
apply (subst if_bool_eq_conj)+
apply (simp split: if_split_asm, safe, simp_all add: arrlist_nth)
apply (rule_tac x = "ee" in exI)
apply (subgoal_tac "num_vertices_C (heap_IGraph_C s g) \<le> fst (snd (snd iG) ee)")
apply force
apply (subgoal_tac "first_C (heap_IEdge_C s (arcs_C (heap_IGraph_C s g) +\<^sub>p uint ee)) = fst (snd (snd iG) ee)")
apply simp
apply (subst tail_heap[where iG=iG], simp)
apply blast
apply blast
apply(rule_tac x = "ee" in exI)
apply (subgoal_tac "num_vertices_C (heap_IGraph_C s g) \<le> snd (snd (snd iG) ee)")
apply force
apply (subgoal_tac "second_C (heap_IEdge_C s (arcs_C (heap_IGraph_C s g) +\<^sub>p uint ee)) = snd (snd (snd iG) ee)")
apply simp
apply (subst head_heap[where iG=iG], simp)
apply blast
apply blast
apply (metis edge_heap s_C_pte le_cases le_step uint_nat word_le_less_eq)
apply (metis head_heap le_step not_less)
apply (simp add: le_step word_not_le)
using le_step not_less
apply blast
apply (metis (mono_tags, hide_lams) diff_diff_add diff_self_eq_0 eq_iff_diff_eq_0 measure_unat not_less0 word_less_nat_alt zero_less_diff)
apply (rule arrlist_nth, (simp add: uint_nat unat_mono)+)
apply wp
apply fast
done
definition trian_inv :: "IGraph \<Rightarrow> IDist \<Rightarrow> ICost \<Rightarrow> 32 word \<Rightarrow> bool" where
"trian_inv G d c m \<equiv>
\<forall>i < m. d (snd (iedges G i)) \<le> d (fst (iedges G i)) + c i"
lemma trian_spc':
"\<lbrace> P and
(\<lambda>s. wf_digraph (abs_IGraph iG) \<and>
is_graph s iG g \<and>
is_dist s iG iD d \<and>
is_cost s iG iC c)\<rbrace>
trian' g d c
\<lbrace> (\<lambda>_ s. P s) And
(\<lambda>rr s. rr \<noteq> 0 \<longleftrightarrow> trian_inv iG iD iC (iedge_cnt iG)) \<rbrace>!"
apply (clarsimp simp: trian'_def)
apply (subst whileLoopE_add_inv [where
M="\<lambda>(ee, s). unat (iedge_cnt iG - ee)" and
I="\<lambda>ee s. P s \<and> trian_inv iG iD iC ee \<and>
ee \<le> iedge_cnt iG \<and>
wf_digraph (abs_IGraph iG) \<and>
is_graph s iG g \<and>
is_dist s iG iD d \<and>
is_cost s iG iC c"])
apply (simp add: skipE_def)
apply wp
unfolding is_graph_def is_dist_def is_cost_def trian_inv_def
apply (subst if_bool_eq_conj)+
apply (simp split: if_split_asm, safe, simp_all add: arrlist_nth)
apply (rule_tac x = "ee" in exI)
apply (rule conjI, simp+)
apply (subst pedge_num_dist_heap_ptr_coerce[where l=d and iL=iD])
apply fast
apply (subst head_heap[where iG=iG], simp+)
apply (metis head_heap wellformed_iGraph, simp+)
apply (subst pedge_num_dist_heap_ptr_coerce[where l=d and iL=iD])
apply fast
apply (subst tail_heap[where iG=iG], simp+)
apply (metis tail_heap wellformed_iGraph, simp+)
apply (drule wellformed_iGraph[where G=iG])
apply simp+
apply (subst head_heap[where iG=iG], simp+)
apply (subst tail_heap[where iG=iG], simp+)
apply (subgoal_tac "heap_w32 s (ptr_coerce (d +\<^sub>p int (unat (second_C (heap_IEdge_C s (arcs_C (heap_IGraph_C s g) +\<^sub>p uint ee))))))
> heap_w32 s (ptr_coerce (d +\<^sub>p int (unat (first_C (heap_IEdge_C s (arcs_C (heap_IGraph_C s g) +\<^sub>p uint ee)))))) + iC ee")
apply simp+
apply (subst pedge_num_dist_heap[where l=c and iL=iC])
apply simp+
apply (metis uint_nat)
apply (subst pedge_num_dist_heap_ptr_coerce[where l=d and iL=iD])
apply fast
apply (subst head_heap[where iG=iG], simp+)
using le_step less_trans
apply blast
apply (metis (no_types, hide_lams) head_heap wellformed_iGraph le_step less_trans)
using word_zero_le
apply blast
apply (subst pedge_num_dist_heap_ptr_coerce[where l=d and iL=iD])
apply fast
apply (subst tail_heap[where iG=iG], simp+)
using le_step less_trans
apply blast
apply (metis (no_types, hide_lams) tail_heap wellformed_iGraph le_step less_trans)
apply simp
apply (subst pedge_num_dist_heap[where l=c and iL=iC])
apply (simp add: uint_nat)+
using le_step less_trans
apply blast
apply (subst head_heap[where iG=iG], simp+)
using le_step less_trans
apply blast
apply (subst tail_heap[where iG=iG], simp+)
using le_step less_trans
apply blast
apply (subgoal_tac "i < num_edges_C (heap_IGraph_C s g)")
apply (subgoal_tac "\<And>w. \<not> w < num_edges_C (heap_IGraph_C s g) \<or> heap_w32 s (c +\<^sub>p uint w) = iC w")
apply (subgoal_tac "\<And>w. \<not> w < num_edges_C (heap_IGraph_C s g) \<or> heap_IEdge_C s (arcs_C (heap_IGraph_C s g) +\<^sub>p uint w) = to_edge (snd (snd iG) w)")
apply (subgoal_tac "\<And>w. \<not> w < fst iG \<or> heap_w32 s (ptr_coerce (d +\<^sub>p uint w)) = iD w")
apply (subgoal_tac "\<And>w. \<not> w < num_edges_C (heap_IGraph_C s g) \<or> snd (snd (snd iG) w) < fst iG")
apply (subgoal_tac "\<And>w. \<not> w < num_edges_C (heap_IGraph_C s g) \<or> fst (snd (snd iG) w) < fst iG")
apply (subgoal_tac "heap_w32 s (ptr_coerce (d +\<^sub>p int (unat (second_C (heap_IEdge_C s (arcs_C (heap_IGraph_C s g) +\<^sub>p uint i)))))) \<le> heap_w32 s (ptr_coerce (d +\<^sub>p int (unat (first_C (heap_IEdge_C s (arcs_C (heap_IGraph_C s g) +\<^sub>p uint i)))))) + heap_w32 s (c +\<^sub>p int (unat i))")
apply metis
apply (subgoal_tac "\<forall>w. heap_w32 s (ptr_coerce (d +\<^sub>p int (unat w))) = iD w \<or> \<not> w < fst iG")
apply (subgoal_tac "heap_w32 s (ptr_coerce (d +\<^sub>p int (unat (second_C (heap_IEdge_C s (arcs_C (heap_IGraph_C s g) +\<^sub>p int (unat i))))))) \<le> heap_w32 s (ptr_coerce (d +\<^sub>p int (unat (first_C (heap_IEdge_C s (arcs_C (heap_IGraph_C s g) +\<^sub>p int (unat i))))))) + iC i")
apply (subgoal_tac "heap_w32 s (ptr_coerce (d +\<^sub>p int (unat (second_C (heap_IEdge_C s (arcs_C (heap_IGraph_C s g) +\<^sub>p uint i)))))) \<le> heap_w32 s (ptr_coerce (d +\<^sub>p int (unat (first_C (heap_IEdge_C s (arcs_C (heap_IGraph_C s g) +\<^sub>p uint i)))))) + heap_w32 s (c +\<^sub>p int (unat i))")
apply (simp add:uint_nat)+
apply (metis (no_types, hide_lams) le_step word_not_le)
apply (metis uint_nat)
apply (simp add: wf_digraph_def)
apply (simp add: wf_digraph_def)
apply (simp add: pedge_num_dist_heap_ptr_coerce uint_nat)
apply (simp add: edge_heap uint_nat)
apply (simp add: pedge_num_dist_heap uint_nat)
using le_step less_trans
apply blast
using le_step not_less
apply blast
apply (metis (no_types, hide_lams) diff_diff_add eq_iff_diff_eq_0 measure_unat word_not_le)
apply (rule arrlist_nth, (simp add: uint_nat unat_mono)+)
apply (metis tail_heap wellformed_iGraph uint_nat word_less_nat_alt)
apply (rule_tac i="uint ee" in arrlist_nth_valid, simp+)
apply (simp add:uint_nat)
using word_less_nat_alt
apply blast
apply (rule arrlist_nth, (simp add: uint_nat unat_mono)+)
apply (metis head_heap wellformed_iGraph uint_nat word_less_nat_alt)
apply (rule arrlist_nth, (simp add: uint_nat unat_mono)+)
apply wp
apply fast
done
definition just_inv ::
"IGraph \<Rightarrow> IDist \<Rightarrow> ICost \<Rightarrow> IVertex \<Rightarrow> INum \<Rightarrow> IPEdge \<Rightarrow> 32 word \<Rightarrow> bool" where
"just_inv G d c s n p k \<equiv>
\<forall>v < k. v \<noteq> s \<and> n v \<ge> 0 \<longrightarrow>
(\<exists> e. e = p v (*\<and> p v \<ge> 0*) \<and> e < iedge_cnt G \<and>
v = snd (iedges G e) \<and>
d v = d (fst (iedges G e)) + c e \<and>
n v = n (fst (iedges G e)) + 1)"
lemma just_inv_step:
assumes v_less_max: "v < max_word"
shows "just_inv G d c s n p (v + 1) \<longleftrightarrow> just_inv G d c s n p v
\<and> (v \<noteq> s \<and> n v \<ge> 0 \<longrightarrow>
(\<exists> e. e = (p v) \<and> e < iedge_cnt G \<and>
v = snd (iedges G e) \<and>
d v = d (fst (iedges G e)) + c e \<and>
n v = n (fst (iedges G e)) + 1))"
unfolding just_inv_def using v_less_max
by (auto simp add : less_x_plus_1)
lemma just_inv_le:
assumes leq: "j \<le> i"
assumes just_i: "just_inv G d c s n p i"
shows "just_inv G d c s n p j"
using assms
by (induct j) (auto simp add: just_inv_def)
lemma not_just_verts:
fixes G R c d n p s v
assumes v_less_max: "v < max_word"
assumes "v < ivertex_cnt G"
assumes "v \<noteq> s \<and> n v \<ge> 0 \<and>
(iedge_cnt G \<le> p v \<or>
snd (iedges G (p v)) \<noteq> v \<or>
d v \<noteq>
d (fst (iedges G (p v))) + c (p v) \<or>
n v \<noteq> n (fst (iedges G (p v))) + 1)"
shows "\<not> just_inv G d c s n p (ivertex_cnt G)"
proof (rule notI)
assume jv: "just_inv G d c s n p (ivertex_cnt G)"
have "just_inv G d c s n p (v + 1)"
by (metis le_step order.asym word_not_le just_inv_le[OF _ jv] assms(2))
then have "(v \<noteq> s \<and> n v \<ge> 0 \<longrightarrow>
(\<exists> e. e = p v \<and> e < iedge_cnt G \<and>
v = snd (iedges G e) \<and>
d v = d (fst (iedges G e)) + c e \<and>
n v = n (fst (iedges G e)) + 1))"
unfolding just_inv_def
using v_less_max just_inv_step
by (auto simp add : less_x_plus_1)
with assms show False by force
qed
lemma just_spc':
"\<lbrace> P and
(\<lambda>s. wf_digraph (abs_IGraph iG) \<and>
is_graph s iG g \<and>
is_dist s iG iD d \<and>
is_cost s iG iC c \<and>
sc < ivertex_cnt iG \<and>
is_numm s iG iN n \<and>
is_pedge s iG iP p)\<rbrace>
just' g d c sc n p
\<lbrace> (\<lambda>_ s. P s) And
(\<lambda>rr s. rr \<noteq> 0 \<longleftrightarrow> just_inv iG iD iC sc iN iP (ivertex_cnt iG)) \<rbrace>!"
apply (clarsimp simp: just'_def)
apply (subst whileLoopE_add_inv [where
M="\<lambda>(vv, s). unat (ivertex_cnt iG - vv)" and
I="\<lambda>vv s. P s \<and> just_inv iG iD iC sc iN iP vv \<and>
vv \<le> ivertex_cnt iG \<and>
wf_digraph (abs_IGraph iG) \<and>
is_graph s iG g \<and>
is_dist s iG iD d \<and>
is_cost s iG iC c \<and>
sc < ivertex_cnt iG \<and>
is_numm s iG iN n \<and>
is_pedge s iG iP p"])
apply (simp add: skipE_def)
apply wp
unfolding is_graph_def is_dist_def is_cost_def is_numm_def is_pedge_def just_inv_def
apply (subst if_bool_eq_conj)+
apply (simp split: if_split_asm, simp_all add: arrlist_nth)
apply (safe)
apply (metis pedge_num_dist_heap_ptr_coerce uint_nat word_not_le word_zero_le)
apply (metis (no_types) head_heap pedge_num_dist_heap_ptr_coerce uint_nat word_zero_le)
prefer 52
apply wp
apply force
prefer 51
apply force
prefer 50
apply (rule_tac i="(uint sc)" in arrlist_nth_valid, simp+)
apply (simp add: uint_nat word_less_def)
prefer 49
apply (metis (no_types, hide_lams) diff_diff_add eq_iff_diff_eq_0 measure_unat word_not_le)
prefer 48
apply argo
prefer 47
apply argo
prefer 46
apply argo
prefer 45
apply argo
prefer 44
apply argo
prefer 43
apply (metis (mono_tags, hide_lams) le_step not_less)
prefer 42
using le_step
apply blast
prefer 41
using le_step
apply blast
prefer 40
using le_step
apply blast
prefer 39
using le_step
apply metis
prefer 38
apply (rule_tac i="(uint vv)" in arrlist_nth_valid, simp+)
apply (simp add: uint_nat word_less_def)
prefer 37
apply (rule_tac i="(uint vv)" in arrlist_nth_valid, simp+)
apply (simp add: uint_nat word_less_def)
prefer 36
apply (metis (no_types, hide_lams) diff_diff_add eq_iff_diff_eq_0 measure_unat word_not_le)
prefer 35
apply argo
prefer 34
apply argo
prefer 33
apply presburger
prefer 32
apply argo
prefer 31
apply argo
prefer 30
apply presburger
prefer 29
apply (metis (mono_tags, hide_lams) le_step not_less)
prefer 28
prefer 27
prefer 26
prefer 25
prefer 24
apply (rule_tac i="(uint vv)" in arrlist_nth_valid, simp+)
apply (simp add: uint_nat word_less_def)
prefer 23
prefer 22
prefer 21
apply (rule_tac i="(uint vv)" in arrlist_nth_valid, simp+)
apply (simp add: uint_nat word_less_def)
prefer 20
apply (metis (mono_tags, hide_lams) diff_diff_add eq_iff_diff_eq_0 measure_unat word_not_le)
prefer 19
apply argo
prefer 18
apply argo
prefer 17
apply presburger
prefer 16
apply argo
prefer 15
apply argo
prefer 14
apply argo
prefer 13
apply (metis le_step not_less)
prefer 12
prefer 11
apply (metis (no_types) edge_heap pedge_num_dist_heap_ptr_coerce t_C_pte le_step not_less uint_nat word_zero_le)
prefer 10
apply (metis (no_types) pedge_num_dist_heap_ptr_coerce le_step not_less uint_nat word_zero_le)
prefer 9
apply (subgoal_tac "\<forall>w. heap_w32 s (ptr_coerce (p +\<^sub>p int (unat w))) = iP w \<or> \<not> w < fst iG")
apply (subgoal_tac "\<forall>w. heap_w32 s (ptr_coerce (n +\<^sub>p int (unat w))) = iN w \<or> \<not> w < fst iG")
apply (subgoal_tac "\<exists>w<num_vertices_C (heap_IGraph_C s g). w \<noteq> sc \<and> (iD w = iD (fst (snd (snd iG) (iP w))) + iC (iP w) \<longrightarrow> w = snd (snd (snd iG) (iP w)) \<longrightarrow> iP w < num_edges_C (heap_IGraph_C s g) \<longrightarrow> iN w \<noteq> iN (fst (snd (snd iG) (iP w))) + 1)")
apply (metis (no_types))
apply (metis (no_types, hide_lams) tail_heap wellformed_iGraph uint_nat)
apply (metis pedge_num_dist_heap_ptr_coerce word_zero_le)
apply (metis pedge_num_dist_heap_ptr_coerce word_zero_le)
apply (subst pedge_num_dist_heap_ptr_coerce[where l=p and iL=iP])
apply simp+
using le_step less_trans
apply blast
apply fastforce
apply (subst pedge_num_dist_heap_ptr_coerce[where l=n and iL=iN])
apply simp+
using le_step less_trans
apply blast
apply fastforce
apply (subst pedge_num_dist_heap_ptr_coerce[where l=n and iL=iN])
apply simp+
apply (metis (no_types) pedge_num_dist_heap_ptr_coerce wellformed_iGraph le_step uint_nat word_not_le word_zero_le)
apply fastforce
apply (subgoal_tac "\<forall>w. heap_w32 s (ptr_coerce (p +\<^sub>p int (unat w))) = iP w \<or> \<not> w < fst iG")
apply (subgoal_tac "\<forall>w. heap_w32 s (ptr_coerce (n +\<^sub>p int (unat w))) = iN w \<or> \<not> w < fst iG")
apply (subgoal_tac "heap_w32 s (ptr_coerce (p +\<^sub>p int (unat vv))) < fst (snd iG)")
apply (subgoal_tac "heap_w32 s (ptr_coerce (n +\<^sub>p int (unat v))) = heap_w32 s (ptr_coerce (n +\<^sub>p int (unat (fst (snd (snd iG) (heap_w32 s (ptr_coerce (p +\<^sub>p int (unat v))))))))) + 1")
apply (metis (no_types))
apply (metis (no_types, hide_lams) edge_heap s_C_pte wellformed_iGraph le_step uint_nat)
apply (simp add:uint_nat)
apply (metis pedge_num_dist_heap_ptr_coerce word_zero_le)
apply (metis pedge_num_dist_heap_ptr_coerce word_zero_le)
prefer 8
apply (subst pedge_num_dist_heap_ptr_coerce[where l=d and iL=iD], simp+)
using le_step less_trans
apply blast
apply simp
apply (subst pedge_num_dist_heap_ptr_coerce[where l=p and iL=iP], simp+)
using le_step less_trans
apply blast
apply simp
apply (subst tail_heap[where iG=iG], simp+)
apply (subgoal_tac "\<forall>w. w < num_vertices_C (heap_IGraph_C s g) \<or> \<not> w < vv")
apply (subgoal_tac "heap_w32 s (ptr_coerce (p +\<^sub>p int (unat v))) < num_edges_C (heap_IGraph_C s g)")
apply (meson less_trans)
apply (metis (no_types) pedge_num_dist_heap_ptr_coerce le_step not_less uint_nat word_zero_le)
apply fastforce
apply (subst pedge_num_dist_heap_ptr_coerce[where l=d and iL=iD], simp+)
apply (subgoal_tac "\<forall>w. heap_w32 s (ptr_coerce (p +\<^sub>p int (unat w))) = iP w \<or> \<not> w < fst iG")
apply (subgoal_tac "first_C (heap_IEdge_C s (arcs_C (heap_IGraph_C s g) +\<^sub>p uint (heap_w32 s (ptr_coerce (p +\<^sub>p int (unat v)))))) < num_vertices_C (heap_IGraph_C s g)")
using pedge_num_dist_heap_ptr_coerce
apply fastforce
apply (metis (no_types) tail_heap wellformed_iGraph le_step not_less uint_nat)
apply (metis pedge_num_dist_heap_ptr_coerce word_zero_le)
apply force
apply (subst pedge_num_dist_heap_ptr_coerce[where l=p and iL=iP], simp+)
using le_step less_trans
apply blast
apply simp
apply (subst pedge_num_dist_heap[where l=c and iL=iC], simp+)
apply (subgoal_tac "\<forall>w. w < num_vertices_C (heap_IGraph_C s g) \<or> \<not> w < vv")
apply (subgoal_tac "heap_w32 s (ptr_coerce (p +\<^sub>p int (unat v))) < num_edges_C (heap_IGraph_C s g)")
using less_trans
apply blast
apply (metis (no_types) pedge_num_dist_heap_ptr_coerce le_step not_less uint_nat word_zero_le)
using less_trans
apply (blast, clarsimp)
sorry
definition no_path_inv :: "IGraph \<Rightarrow> IDist \<Rightarrow> INum \<Rightarrow> 32 word \<Rightarrow> bool" where
"no_path_inv G d n k \<equiv> \<forall>v < k. (d v < 0 \<longleftrightarrow> n v < 0)"
lemma no_path_inv_step:
"no_path_inv G d n (v + 1) \<longleftrightarrow> no_path_inv G d n v
\<and> (d v < 0 \<longleftrightarrow> n v < 0)"
by (auto simp add: no_path_inv_def)
lemma no_path_spc':
"\<lbrace> P and
(\<lambda>s. wf_digraph (abs_IGraph iG) \<and>
is_graph s iG g \<and>
is_dist s iG iD d \<and>
is_numm s iG iN n)\<rbrace>
no_path' g d n
\<lbrace> (\<lambda>_ s. P s) And
(\<lambda>rr s. rr \<noteq> 0 \<longleftrightarrow> no_path_inv iG iD iN (ivertex_cnt iG)) \<rbrace>!"
apply (clarsimp simp: no_path'_def)
apply (subst whileLoopE_add_inv [where
M="\<lambda>(vv, s). unat (ivertex_cnt iG - vv)" and
I="\<lambda>vv s. P s \<and> no_path_inv iG iD iN vv \<and>
vv \<le> ivertex_cnt iG \<and>
wf_digraph (abs_IGraph iG) \<and>
is_graph s iG g \<and>
is_dist s iG iD d \<and>
is_numm s iG iN n"])
apply (simp add: skipE_def)
apply wp
unfolding is_graph_def is_dist_def is_numm_def no_path_inv_def
apply (subst if_bool_eq_conj)+
apply (simp split: if_split_asm, safe, simp_all add: arrlist_nth)
prefer 10
apply wp
apply fast
prefer 9
apply (rule_tac i="(uint vv)" in arrlist_nth_valid, simp+)
apply (simp add: uint_nat word_less_def)
prefer 6
using le_step not_less
apply blast
prefer 6
apply (metis (no_types, hide_lams) diff_diff_add eq_iff_diff_eq_0 measure_unat word_not_le)
prefer 2
using le_step not_less
apply blast
prefer 2
apply (metis (no_types, hide_lams) diff_diff_add eq_iff_diff_eq_0 measure_unat word_not_le)
prefer 2
apply (rule_tac i="(uint vv)" in arrlist_nth_valid, simp+)
apply (simp add:uint_nat word_less_def)
prefer 3
apply(rule_tac i="(uint vv)" in arrlist_nth_valid, simp+)
apply (simp add:uint_nat word_less_def)
prefer 2
apply (simp add: uint_nat sint_ucast)
apply (rule classical, erule notE, simp)
(*
apply (subgoal_tac "sint (heap_w32 s (ptr_coerce (d +\<^sub>p int (unat vv)))) < 0")
apply force
apply (thin_tac "\<not> sint (heap_w32 s (ptr_coerce (d +\<^sub>p int (unat vv)))) < 0")
apply (drule_tac i=vv in pedge_num_dist_heap_ptr_coerce[where l=d and iL=iD])
apply simp+
apply (drule_tac i=vv in pedge_num_dist_heap_ptr_coerce[where l=n and iL=iN])
apply simp+
*)
(*
apply (subst "sint_eq_uint")
apply (rule not_msb_from_less)
find_theorems(99) "sint _ = uint _"
find_theorems "msb"
*)
sorry
definition pos_cost_inv :: "IGraph \<Rightarrow> ICost \<Rightarrow> 32 word \<Rightarrow> bool" where
"pos_cost_inv G c m \<equiv> \<forall>e < m. c e \<ge> 0"
lemma pos_cost_spc':
"\<lbrace> P and
(\<lambda>s. wf_digraph (abs_IGraph iG) \<and>
is_graph s iG g \<and>
is_cost s iG iC c)\<rbrace>
pos_cost' g c
\<lbrace> (\<lambda>_ s. P s) And
(\<lambda>rr s. rr \<noteq> 0 \<longleftrightarrow> pos_cost_inv iG iC (iedge_cnt iG)) \<rbrace>!"
apply (clarsimp simp: pos_cost'_def)
apply (subst whileLoop_add_inv [where
M="\<lambda>(ee, s). unat (iedge_cnt iG - ee)" and
I="\<lambda>ee s. P s \<and> pos_cost_inv iG iC ee \<and>
ee \<le> iedge_cnt iG \<and>
wf_digraph (abs_IGraph iG) \<and>
is_graph s iG g \<and>
is_cost s iG iC c"])
apply wp
unfolding is_graph_def is_cost_def pos_cost_inv_def
apply (simp split: if_split_asm, safe, simp_all add: arrlist_nth)
using le_step not_less
apply blast
apply (subgoal_tac "num_edges_C (heap_IGraph_C s g) - ee \<noteq> 0")
apply simp
apply (subgoal_tac "\<And>w wa. (w::32 word) - wa = 0 \<or> unat (w - 1 - wa) < unat (w - wa)")
apply (subgoal_tac "unat (num_edges_C (heap_IGraph_C s g) - 1 - ee) < unat (num_edges_C (heap_IGraph_C s g) - ee)")
apply (subgoal_tac "unat (num_edges_C (heap_IGraph_C s g) - (ee + 1)) < unat (num_edges_C (heap_IGraph_C s g) - ee)")
apply (simp add: add.commute diff_diff_add)
apply (simp add: diff_add_eq_diff_diff_swap)
apply fastforce
apply (metis (no_types) add.commute diff_diff_add measure_unat)
apply simp
apply (rule_tac i="(uint ee)" in arrlist_nth_valid, simp+)
apply (simp add: uint_nat word_less_def)
apply wp
apply fast
done
end
end