diff --git a/theories/lithium/simpl_instances.v b/theories/lithium/simpl_instances.v
index 82d38d50b572328f726f9c339478af8f895edfab..5786737af1737403296fe5d492cb56b6687f8c7d 100644
--- a/theories/lithium/simpl_instances.v
+++ b/theories/lithium/simpl_instances.v
@@ -39,6 +39,10 @@ Proof. split; destruct l; naive_solver. Qed.
Global Instance simpl_to_cons_Some A (l : list A) x : SimplBothRel (=) (maybe2 cons l) (Some x) (l = x.1::x.2).
Proof. split; destruct l, x; naive_solver. Qed.
+Global Instance simpl_protected_neq_nil A (l : list A) `{!IsProtected l} :
+ SimplBoth (l ≠[]) (∃ x l', l = x :: l').
+Proof. split; destruct l; naive_solver. Qed.
+
Global Instance simpl_gt_0_neg n : SimplBoth (¬ (0 < n))%nat (n = 0%nat).
Proof. split; destruct n; naive_solver lia. Qed.
diff --git a/tutorial/proofs/quicksort_exercise/generated_code.v b/tutorial/proofs/quicksort_exercise/generated_code.v
index e43d90b0ee6478a4d7393a3dc41c0b98008437d4..f096b27cabb14abbf927c99eb55ae3d720abb1d2 100644
--- a/tutorial/proofs/quicksort_exercise/generated_code.v
+++ b/tutorial/proofs/quicksort_exercise/generated_code.v
@@ -65,14 +65,14 @@ Section code.
Definition loc_60 : location_info := LocationInfo file_0 40 13 40 17.
Definition loc_61 : location_info := LocationInfo file_0 40 13 40 17.
Definition loc_62 : location_info := LocationInfo file_0 35 7 35 25.
- Definition loc_63 : location_info := LocationInfo file_0 35 7 35 16.
- Definition loc_64 : location_info := LocationInfo file_0 35 7 35 16.
- Definition loc_65 : location_info := LocationInfo file_0 35 7 35 11.
- Definition loc_66 : location_info := LocationInfo file_0 35 7 35 11.
- Definition loc_67 : location_info := LocationInfo file_0 35 9 35 10.
- Definition loc_68 : location_info := LocationInfo file_0 35 9 35 10.
- Definition loc_69 : location_info := LocationInfo file_0 35 20 35 25.
- Definition loc_70 : location_info := LocationInfo file_0 35 20 35 25.
+ Definition loc_63 : location_info := LocationInfo file_0 35 7 35 12.
+ Definition loc_64 : location_info := LocationInfo file_0 35 7 35 12.
+ Definition loc_65 : location_info := LocationInfo file_0 35 16 35 25.
+ Definition loc_66 : location_info := LocationInfo file_0 35 16 35 25.
+ Definition loc_67 : location_info := LocationInfo file_0 35 16 35 20.
+ Definition loc_68 : location_info := LocationInfo file_0 35 16 35 20.
+ Definition loc_69 : location_info := LocationInfo file_0 35 18 35 19.
+ Definition loc_70 : location_info := LocationInfo file_0 35 18 35 19.
Definition loc_71 : location_info := LocationInfo file_0 34 18 34 20.
Definition loc_72 : location_info := LocationInfo file_0 34 18 34 20.
Definition loc_73 : location_info := LocationInfo file_0 34 19 34 20.
@@ -94,6 +94,48 @@ Section code.
Definition loc_93 : location_info := LocationInfo file_0 30 6 30 7.
Definition loc_94 : location_info := LocationInfo file_0 30 6 30 7.
Definition loc_95 : location_info := LocationInfo file_0 30 11 30 25.
+ Definition loc_98 : location_info := LocationInfo file_0 46 2 54 3.
+ Definition loc_99 : location_info := LocationInfo file_0 46 27 48 3.
+ Definition loc_100 : location_info := LocationInfo file_0 47 4 47 11.
+ Definition loc_102 : location_info := LocationInfo file_0 48 9 54 3.
+ Definition loc_103 : location_info := LocationInfo file_0 49 4 49 26.
+ Definition loc_104 : location_info := LocationInfo file_0 50 4 50 40.
+ Definition loc_105 : location_info := LocationInfo file_0 51 4 51 23.
+ Definition loc_106 : location_info := LocationInfo file_0 52 4 52 17.
+ Definition loc_107 : location_info := LocationInfo file_0 53 4 53 22.
+ Definition loc_108 : location_info := LocationInfo file_0 53 4 53 10.
+ Definition loc_109 : location_info := LocationInfo file_0 53 4 53 10.
+ Definition loc_110 : location_info := LocationInfo file_0 53 11 53 12.
+ Definition loc_111 : location_info := LocationInfo file_0 53 11 53 12.
+ Definition loc_112 : location_info := LocationInfo file_0 53 14 53 20.
+ Definition loc_113 : location_info := LocationInfo file_0 53 14 53 20.
+ Definition loc_114 : location_info := LocationInfo file_0 52 4 52 13.
+ Definition loc_115 : location_info := LocationInfo file_0 52 4 52 13.
+ Definition loc_116 : location_info := LocationInfo file_0 52 14 52 15.
+ Definition loc_117 : location_info := LocationInfo file_0 52 14 52 15.
+ Definition loc_118 : location_info := LocationInfo file_0 51 4 51 13.
+ Definition loc_119 : location_info := LocationInfo file_0 51 4 51 13.
+ Definition loc_120 : location_info := LocationInfo file_0 51 14 51 21.
+ Definition loc_121 : location_info := LocationInfo file_0 51 15 51 21.
+ Definition loc_122 : location_info := LocationInfo file_0 50 20 50 39.
+ Definition loc_123 : location_info := LocationInfo file_0 50 20 50 29.
+ Definition loc_124 : location_info := LocationInfo file_0 50 20 50 29.
+ Definition loc_125 : location_info := LocationInfo file_0 50 30 50 31.
+ Definition loc_126 : location_info := LocationInfo file_0 50 30 50 31.
+ Definition loc_127 : location_info := LocationInfo file_0 50 33 50 38.
+ Definition loc_128 : location_info := LocationInfo file_0 50 33 50 38.
+ Definition loc_131 : location_info := LocationInfo file_0 49 16 49 25.
+ Definition loc_132 : location_info := LocationInfo file_0 49 16 49 25.
+ Definition loc_133 : location_info := LocationInfo file_0 49 16 49 20.
+ Definition loc_134 : location_info := LocationInfo file_0 49 16 49 20.
+ Definition loc_135 : location_info := LocationInfo file_0 49 18 49 19.
+ Definition loc_136 : location_info := LocationInfo file_0 49 18 49 19.
+ Definition loc_139 : location_info := LocationInfo file_0 46 5 46 25.
+ Definition loc_140 : location_info := LocationInfo file_0 46 5 46 7.
+ Definition loc_141 : location_info := LocationInfo file_0 46 5 46 7.
+ Definition loc_142 : location_info := LocationInfo file_0 46 6 46 7.
+ Definition loc_143 : location_info := LocationInfo file_0 46 6 46 7.
+ Definition loc_144 : location_info := LocationInfo file_0 46 11 46 25.
(* Definition of struct [list_node]. *)
Program Definition struct_list_node := {|
@@ -176,7 +218,7 @@ Section code.
"head" <-{ LPtr }
LocInfoE loc_71 (use{LPtr} (LocInfoE loc_73 (!{LPtr} (LocInfoE loc_74 ("l"))))) ;
locinfo: loc_62 ;
- if: LocInfoE loc_62 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_62 ((LocInfoE loc_63 (use{it_layout i32} (LocInfoE loc_64 ((LocInfoE loc_65 (!{LPtr} (LocInfoE loc_67 (!{LPtr} (LocInfoE loc_68 ("l")))))) at{struct_list_node} "val")))) ≤{IntOp i32, IntOp i32} (LocInfoE loc_69 (use{it_layout i32} (LocInfoE loc_70 ("pivot")))))))
+ if: LocInfoE loc_62 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_62 ((LocInfoE loc_63 (use{it_layout i32} (LocInfoE loc_64 ("pivot")))) ≤{IntOp i32, IntOp i32} (LocInfoE loc_65 (use{it_layout i32} (LocInfoE loc_66 ((LocInfoE loc_67 (!{LPtr} (LocInfoE loc_69 (!{LPtr} (LocInfoE loc_70 ("l")))))) at{struct_list_node} "val")))))))
then
locinfo: loc_39 ;
Goto "#3"
@@ -200,4 +242,51 @@ Section code.
]> $∅
)%E
|}.
+
+ (* Definition of function [quicksort]. *)
+ Definition impl_quicksort (append partition quicksort : loc): function := {|
+ f_args := [
+ ("l", LPtr)
+ ];
+ f_local_vars := [
+ ("pivot", it_layout i32);
+ ("higher", LPtr)
+ ];
+ f_init := "#0";
+ f_code := (
+ <[ "#0" :=
+ locinfo: loc_139 ;
+ if: LocInfoE loc_139 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_139 ((LocInfoE loc_140 (use{LPtr} (LocInfoE loc_142 (!{LPtr} (LocInfoE loc_143 ("l")))))) ={PtrOp, PtrOp} (LocInfoE loc_144 (NULL)))))
+ then
+ locinfo: loc_100 ;
+ Goto "#1"
+ else
+ Goto "#2"
+ ]> $
+ <[ "#1" :=
+ locinfo: loc_100 ;
+ Return (VOID)
+ ]> $
+ <[ "#2" :=
+ "pivot" <-{ it_layout i32 }
+ LocInfoE loc_131 (use{it_layout i32} (LocInfoE loc_132 ((LocInfoE loc_133 (!{LPtr} (LocInfoE loc_135 (!{LPtr} (LocInfoE loc_136 ("l")))))) at{struct_list_node} "val"))) ;
+ locinfo: loc_122 ;
+ "$0" <- LocInfoE loc_124 (partition) with
+ [ LocInfoE loc_125 (use{LPtr} (LocInfoE loc_126 ("l"))) ;
+ LocInfoE loc_127 (use{it_layout i32} (LocInfoE loc_128 ("pivot"))) ] ;
+ "higher" <-{ LPtr } LocInfoE loc_122 ("$0") ;
+ locinfo: loc_105 ;
+ "_" <- LocInfoE loc_119 (quicksort) with
+ [ LocInfoE loc_120 (&(LocInfoE loc_121 ("higher"))) ] ;
+ locinfo: loc_106 ;
+ "_" <- LocInfoE loc_115 (quicksort) with
+ [ LocInfoE loc_116 (use{LPtr} (LocInfoE loc_117 ("l"))) ] ;
+ locinfo: loc_107 ;
+ "_" <- LocInfoE loc_109 (append) with
+ [ LocInfoE loc_110 (use{LPtr} (LocInfoE loc_111 ("l"))) ;
+ LocInfoE loc_112 (use{LPtr} (LocInfoE loc_113 ("higher"))) ] ;
+ Return (VOID)
+ ]> $∅
+ )%E
+ |}.
End code.
diff --git a/tutorial/proofs/quicksort_exercise/generated_proof_quicksort.v b/tutorial/proofs/quicksort_exercise/generated_proof_quicksort.v
new file mode 100644
index 0000000000000000000000000000000000000000..7afb1f35aa0bd8cb8cbb6db0695f618c54e91358
--- /dev/null
+++ b/tutorial/proofs/quicksort_exercise/generated_proof_quicksort.v
@@ -0,0 +1 @@
+(* You were too lazy to even write a spec for this function. *)
diff --git a/tutorial/proofs/quicksort_exercise/generated_spec.v b/tutorial/proofs/quicksort_exercise/generated_spec.v
index 1dc22b0b63f673995a6f3c4348b90e89ea7c515f..6846713430ea6d30242b725246d04601e5d3cf80 100644
--- a/tutorial/proofs/quicksort_exercise/generated_spec.v
+++ b/tutorial/proofs/quicksort_exercise/generated_spec.v
@@ -11,4 +11,6 @@ Section spec.
(* Function [append] has been skipped. *)
(* Function [partition] has been skipped. *)
+
+ (* Function [quicksort] has been skipped. *)
End spec.
diff --git a/tutorial/proofs/quicksort_exercise/proof_files b/tutorial/proofs/quicksort_exercise/proof_files
index 0b5500e1fa751b051c84d9e1dec5cfc16c444de8..97f3be09afdc26dbbbdfcfaddd45eb4b45e1b45c 100644
--- a/tutorial/proofs/quicksort_exercise/proof_files
+++ b/tutorial/proofs/quicksort_exercise/proof_files
@@ -1,2 +1,3 @@
generated_proof_append.v
generated_proof_partition.v
+generated_proof_quicksort.v
diff --git a/tutorial/proofs/quicksort_solution/generated_code.v b/tutorial/proofs/quicksort_solution/generated_code.v
index d1f7479cd1a9346a172f654105cac410277bbe8b..44fd2849f8c1784bae3aa5824303a37f5eb7ae6e 100644
--- a/tutorial/proofs/quicksort_solution/generated_code.v
+++ b/tutorial/proofs/quicksort_solution/generated_code.v
@@ -6,94 +6,136 @@ Set Default Proof Using "Type".
(* Generated from [tutorial/quicksort_solution.c]. *)
Section code.
Definition file_0 : string := "tutorial/quicksort_solution.c".
- Definition loc_2 : location_info := LocationInfo file_0 24 2 28 3.
- Definition loc_3 : location_info := LocationInfo file_0 24 27 26 3.
- Definition loc_4 : location_info := LocationInfo file_0 25 4 25 11.
- Definition loc_5 : location_info := LocationInfo file_0 25 4 25 6.
- Definition loc_6 : location_info := LocationInfo file_0 25 5 25 6.
- Definition loc_7 : location_info := LocationInfo file_0 25 5 25 6.
- Definition loc_8 : location_info := LocationInfo file_0 25 9 25 10.
- Definition loc_9 : location_info := LocationInfo file_0 25 9 25 10.
- Definition loc_10 : location_info := LocationInfo file_0 26 9 28 3.
- Definition loc_11 : location_info := LocationInfo file_0 27 4 27 27.
- Definition loc_12 : location_info := LocationInfo file_0 27 4 27 10.
- Definition loc_13 : location_info := LocationInfo file_0 27 4 27 10.
- Definition loc_14 : location_info := LocationInfo file_0 27 11 27 22.
- Definition loc_15 : location_info := LocationInfo file_0 27 12 27 22.
- Definition loc_16 : location_info := LocationInfo file_0 27 12 27 16.
- Definition loc_17 : location_info := LocationInfo file_0 27 12 27 16.
- Definition loc_18 : location_info := LocationInfo file_0 27 14 27 15.
- Definition loc_19 : location_info := LocationInfo file_0 27 14 27 15.
- Definition loc_20 : location_info := LocationInfo file_0 27 24 27 25.
- Definition loc_21 : location_info := LocationInfo file_0 27 24 27 25.
- Definition loc_22 : location_info := LocationInfo file_0 24 5 24 25.
- Definition loc_23 : location_info := LocationInfo file_0 24 5 24 7.
- Definition loc_24 : location_info := LocationInfo file_0 24 5 24 7.
- Definition loc_25 : location_info := LocationInfo file_0 24 6 24 7.
- Definition loc_26 : location_info := LocationInfo file_0 24 6 24 7.
- Definition loc_27 : location_info := LocationInfo file_0 24 11 24 25.
- Definition loc_30 : location_info := LocationInfo file_0 39 2 51 3.
- Definition loc_31 : location_info := LocationInfo file_0 39 27 41 3.
- Definition loc_32 : location_info := LocationInfo file_0 40 4 40 26.
- Definition loc_33 : location_info := LocationInfo file_0 40 11 40 25.
- Definition loc_34 : location_info := LocationInfo file_0 41 9 51 3.
- Definition loc_35 : location_info := LocationInfo file_0 42 4 42 48.
- Definition loc_36 : location_info := LocationInfo file_0 43 4 43 21.
- Definition loc_37 : location_info := LocationInfo file_0 44 4 50 5.
- Definition loc_38 : location_info := LocationInfo file_0 44 27 48 5.
- Definition loc_39 : location_info := LocationInfo file_0 45 6 45 22.
- Definition loc_40 : location_info := LocationInfo file_0 46 6 46 24.
- Definition loc_41 : location_info := LocationInfo file_0 47 6 47 18.
- Definition loc_42 : location_info := LocationInfo file_0 47 13 47 17.
- Definition loc_43 : location_info := LocationInfo file_0 47 13 47 17.
- Definition loc_44 : location_info := LocationInfo file_0 46 6 46 16.
- Definition loc_45 : location_info := LocationInfo file_0 46 6 46 10.
- Definition loc_46 : location_info := LocationInfo file_0 46 6 46 10.
- Definition loc_47 : location_info := LocationInfo file_0 46 19 46 23.
- Definition loc_48 : location_info := LocationInfo file_0 46 19 46 23.
- Definition loc_49 : location_info := LocationInfo file_0 45 6 45 8.
- Definition loc_50 : location_info := LocationInfo file_0 45 7 45 8.
- Definition loc_51 : location_info := LocationInfo file_0 45 7 45 8.
- Definition loc_52 : location_info := LocationInfo file_0 45 11 45 21.
- Definition loc_53 : location_info := LocationInfo file_0 45 11 45 21.
- Definition loc_54 : location_info := LocationInfo file_0 45 11 45 15.
- Definition loc_55 : location_info := LocationInfo file_0 45 11 45 15.
- Definition loc_56 : location_info := LocationInfo file_0 45 13 45 14.
- Definition loc_57 : location_info := LocationInfo file_0 45 13 45 14.
- Definition loc_58 : location_info := LocationInfo file_0 48 11 50 5.
- Definition loc_59 : location_info := LocationInfo file_0 49 6 49 18.
- Definition loc_60 : location_info := LocationInfo file_0 49 13 49 17.
- Definition loc_61 : location_info := LocationInfo file_0 49 13 49 17.
- Definition loc_62 : location_info := LocationInfo file_0 44 7 44 25.
- Definition loc_63 : location_info := LocationInfo file_0 44 7 44 16.
- Definition loc_64 : location_info := LocationInfo file_0 44 7 44 16.
- Definition loc_65 : location_info := LocationInfo file_0 44 7 44 11.
- Definition loc_66 : location_info := LocationInfo file_0 44 7 44 11.
- Definition loc_67 : location_info := LocationInfo file_0 44 9 44 10.
- Definition loc_68 : location_info := LocationInfo file_0 44 9 44 10.
- Definition loc_69 : location_info := LocationInfo file_0 44 20 44 25.
- Definition loc_70 : location_info := LocationInfo file_0 44 20 44 25.
- Definition loc_71 : location_info := LocationInfo file_0 43 18 43 20.
- Definition loc_72 : location_info := LocationInfo file_0 43 18 43 20.
- Definition loc_73 : location_info := LocationInfo file_0 43 19 43 20.
- Definition loc_74 : location_info := LocationInfo file_0 43 19 43 20.
- Definition loc_77 : location_info := LocationInfo file_0 42 18 42 47.
- Definition loc_78 : location_info := LocationInfo file_0 42 18 42 27.
- Definition loc_79 : location_info := LocationInfo file_0 42 18 42 27.
- Definition loc_80 : location_info := LocationInfo file_0 42 28 42 39.
- Definition loc_81 : location_info := LocationInfo file_0 42 29 42 39.
- Definition loc_82 : location_info := LocationInfo file_0 42 29 42 33.
- Definition loc_83 : location_info := LocationInfo file_0 42 29 42 33.
- Definition loc_84 : location_info := LocationInfo file_0 42 31 42 32.
- Definition loc_85 : location_info := LocationInfo file_0 42 31 42 32.
- Definition loc_86 : location_info := LocationInfo file_0 42 41 42 46.
- Definition loc_87 : location_info := LocationInfo file_0 42 41 42 46.
- Definition loc_90 : location_info := LocationInfo file_0 39 5 39 25.
- Definition loc_91 : location_info := LocationInfo file_0 39 5 39 7.
- Definition loc_92 : location_info := LocationInfo file_0 39 5 39 7.
- Definition loc_93 : location_info := LocationInfo file_0 39 6 39 7.
- Definition loc_94 : location_info := LocationInfo file_0 39 6 39 7.
- Definition loc_95 : location_info := LocationInfo file_0 39 11 39 25.
+ Definition loc_2 : location_info := LocationInfo file_0 26 2 30 3.
+ Definition loc_3 : location_info := LocationInfo file_0 26 27 28 3.
+ Definition loc_4 : location_info := LocationInfo file_0 27 4 27 11.
+ Definition loc_5 : location_info := LocationInfo file_0 27 4 27 6.
+ Definition loc_6 : location_info := LocationInfo file_0 27 5 27 6.
+ Definition loc_7 : location_info := LocationInfo file_0 27 5 27 6.
+ Definition loc_8 : location_info := LocationInfo file_0 27 9 27 10.
+ Definition loc_9 : location_info := LocationInfo file_0 27 9 27 10.
+ Definition loc_10 : location_info := LocationInfo file_0 28 9 30 3.
+ Definition loc_11 : location_info := LocationInfo file_0 29 4 29 27.
+ Definition loc_12 : location_info := LocationInfo file_0 29 4 29 10.
+ Definition loc_13 : location_info := LocationInfo file_0 29 4 29 10.
+ Definition loc_14 : location_info := LocationInfo file_0 29 11 29 22.
+ Definition loc_15 : location_info := LocationInfo file_0 29 12 29 22.
+ Definition loc_16 : location_info := LocationInfo file_0 29 12 29 16.
+ Definition loc_17 : location_info := LocationInfo file_0 29 12 29 16.
+ Definition loc_18 : location_info := LocationInfo file_0 29 14 29 15.
+ Definition loc_19 : location_info := LocationInfo file_0 29 14 29 15.
+ Definition loc_20 : location_info := LocationInfo file_0 29 24 29 25.
+ Definition loc_21 : location_info := LocationInfo file_0 29 24 29 25.
+ Definition loc_22 : location_info := LocationInfo file_0 26 5 26 25.
+ Definition loc_23 : location_info := LocationInfo file_0 26 5 26 7.
+ Definition loc_24 : location_info := LocationInfo file_0 26 5 26 7.
+ Definition loc_25 : location_info := LocationInfo file_0 26 6 26 7.
+ Definition loc_26 : location_info := LocationInfo file_0 26 6 26 7.
+ Definition loc_27 : location_info := LocationInfo file_0 26 11 26 25.
+ Definition loc_30 : location_info := LocationInfo file_0 41 2 53 3.
+ Definition loc_31 : location_info := LocationInfo file_0 41 27 43 3.
+ Definition loc_32 : location_info := LocationInfo file_0 42 4 42 26.
+ Definition loc_33 : location_info := LocationInfo file_0 42 11 42 25.
+ Definition loc_34 : location_info := LocationInfo file_0 43 9 53 3.
+ Definition loc_35 : location_info := LocationInfo file_0 44 4 44 48.
+ Definition loc_36 : location_info := LocationInfo file_0 45 4 45 21.
+ Definition loc_37 : location_info := LocationInfo file_0 46 4 52 5.
+ Definition loc_38 : location_info := LocationInfo file_0 46 27 50 5.
+ Definition loc_39 : location_info := LocationInfo file_0 47 6 47 22.
+ Definition loc_40 : location_info := LocationInfo file_0 48 6 48 24.
+ Definition loc_41 : location_info := LocationInfo file_0 49 6 49 18.
+ Definition loc_42 : location_info := LocationInfo file_0 49 13 49 17.
+ Definition loc_43 : location_info := LocationInfo file_0 49 13 49 17.
+ Definition loc_44 : location_info := LocationInfo file_0 48 6 48 16.
+ Definition loc_45 : location_info := LocationInfo file_0 48 6 48 10.
+ Definition loc_46 : location_info := LocationInfo file_0 48 6 48 10.
+ Definition loc_47 : location_info := LocationInfo file_0 48 19 48 23.
+ Definition loc_48 : location_info := LocationInfo file_0 48 19 48 23.
+ Definition loc_49 : location_info := LocationInfo file_0 47 6 47 8.
+ Definition loc_50 : location_info := LocationInfo file_0 47 7 47 8.
+ Definition loc_51 : location_info := LocationInfo file_0 47 7 47 8.
+ Definition loc_52 : location_info := LocationInfo file_0 47 11 47 21.
+ Definition loc_53 : location_info := LocationInfo file_0 47 11 47 21.
+ Definition loc_54 : location_info := LocationInfo file_0 47 11 47 15.
+ Definition loc_55 : location_info := LocationInfo file_0 47 11 47 15.
+ Definition loc_56 : location_info := LocationInfo file_0 47 13 47 14.
+ Definition loc_57 : location_info := LocationInfo file_0 47 13 47 14.
+ Definition loc_58 : location_info := LocationInfo file_0 50 11 52 5.
+ Definition loc_59 : location_info := LocationInfo file_0 51 6 51 18.
+ Definition loc_60 : location_info := LocationInfo file_0 51 13 51 17.
+ Definition loc_61 : location_info := LocationInfo file_0 51 13 51 17.
+ Definition loc_62 : location_info := LocationInfo file_0 46 7 46 25.
+ Definition loc_63 : location_info := LocationInfo file_0 46 7 46 12.
+ Definition loc_64 : location_info := LocationInfo file_0 46 7 46 12.
+ Definition loc_65 : location_info := LocationInfo file_0 46 16 46 25.
+ Definition loc_66 : location_info := LocationInfo file_0 46 16 46 25.
+ Definition loc_67 : location_info := LocationInfo file_0 46 16 46 20.
+ Definition loc_68 : location_info := LocationInfo file_0 46 16 46 20.
+ Definition loc_69 : location_info := LocationInfo file_0 46 18 46 19.
+ Definition loc_70 : location_info := LocationInfo file_0 46 18 46 19.
+ Definition loc_71 : location_info := LocationInfo file_0 45 18 45 20.
+ Definition loc_72 : location_info := LocationInfo file_0 45 18 45 20.
+ Definition loc_73 : location_info := LocationInfo file_0 45 19 45 20.
+ Definition loc_74 : location_info := LocationInfo file_0 45 19 45 20.
+ Definition loc_77 : location_info := LocationInfo file_0 44 18 44 47.
+ Definition loc_78 : location_info := LocationInfo file_0 44 18 44 27.
+ Definition loc_79 : location_info := LocationInfo file_0 44 18 44 27.
+ Definition loc_80 : location_info := LocationInfo file_0 44 28 44 39.
+ Definition loc_81 : location_info := LocationInfo file_0 44 29 44 39.
+ Definition loc_82 : location_info := LocationInfo file_0 44 29 44 33.
+ Definition loc_83 : location_info := LocationInfo file_0 44 29 44 33.
+ Definition loc_84 : location_info := LocationInfo file_0 44 31 44 32.
+ Definition loc_85 : location_info := LocationInfo file_0 44 31 44 32.
+ Definition loc_86 : location_info := LocationInfo file_0 44 41 44 46.
+ Definition loc_87 : location_info := LocationInfo file_0 44 41 44 46.
+ Definition loc_90 : location_info := LocationInfo file_0 41 5 41 25.
+ Definition loc_91 : location_info := LocationInfo file_0 41 5 41 7.
+ Definition loc_92 : location_info := LocationInfo file_0 41 5 41 7.
+ Definition loc_93 : location_info := LocationInfo file_0 41 6 41 7.
+ Definition loc_94 : location_info := LocationInfo file_0 41 6 41 7.
+ Definition loc_95 : location_info := LocationInfo file_0 41 11 41 25.
+ Definition loc_98 : location_info := LocationInfo file_0 63 2 71 3.
+ Definition loc_99 : location_info := LocationInfo file_0 63 27 65 3.
+ Definition loc_100 : location_info := LocationInfo file_0 64 4 64 11.
+ Definition loc_102 : location_info := LocationInfo file_0 65 9 71 3.
+ Definition loc_103 : location_info := LocationInfo file_0 66 4 66 26.
+ Definition loc_104 : location_info := LocationInfo file_0 67 4 67 40.
+ Definition loc_105 : location_info := LocationInfo file_0 68 4 68 23.
+ Definition loc_106 : location_info := LocationInfo file_0 69 4 69 17.
+ Definition loc_107 : location_info := LocationInfo file_0 70 4 70 22.
+ Definition loc_108 : location_info := LocationInfo file_0 70 4 70 10.
+ Definition loc_109 : location_info := LocationInfo file_0 70 4 70 10.
+ Definition loc_110 : location_info := LocationInfo file_0 70 11 70 12.
+ Definition loc_111 : location_info := LocationInfo file_0 70 11 70 12.
+ Definition loc_112 : location_info := LocationInfo file_0 70 14 70 20.
+ Definition loc_113 : location_info := LocationInfo file_0 70 14 70 20.
+ Definition loc_114 : location_info := LocationInfo file_0 69 4 69 13.
+ Definition loc_115 : location_info := LocationInfo file_0 69 4 69 13.
+ Definition loc_116 : location_info := LocationInfo file_0 69 14 69 15.
+ Definition loc_117 : location_info := LocationInfo file_0 69 14 69 15.
+ Definition loc_118 : location_info := LocationInfo file_0 68 4 68 13.
+ Definition loc_119 : location_info := LocationInfo file_0 68 4 68 13.
+ Definition loc_120 : location_info := LocationInfo file_0 68 14 68 21.
+ Definition loc_121 : location_info := LocationInfo file_0 68 15 68 21.
+ Definition loc_122 : location_info := LocationInfo file_0 67 20 67 39.
+ Definition loc_123 : location_info := LocationInfo file_0 67 20 67 29.
+ Definition loc_124 : location_info := LocationInfo file_0 67 20 67 29.
+ Definition loc_125 : location_info := LocationInfo file_0 67 30 67 31.
+ Definition loc_126 : location_info := LocationInfo file_0 67 30 67 31.
+ Definition loc_127 : location_info := LocationInfo file_0 67 33 67 38.
+ Definition loc_128 : location_info := LocationInfo file_0 67 33 67 38.
+ Definition loc_131 : location_info := LocationInfo file_0 66 16 66 25.
+ Definition loc_132 : location_info := LocationInfo file_0 66 16 66 25.
+ Definition loc_133 : location_info := LocationInfo file_0 66 16 66 20.
+ Definition loc_134 : location_info := LocationInfo file_0 66 16 66 20.
+ Definition loc_135 : location_info := LocationInfo file_0 66 18 66 19.
+ Definition loc_136 : location_info := LocationInfo file_0 66 18 66 19.
+ Definition loc_139 : location_info := LocationInfo file_0 63 5 63 25.
+ Definition loc_140 : location_info := LocationInfo file_0 63 5 63 7.
+ Definition loc_141 : location_info := LocationInfo file_0 63 5 63 7.
+ Definition loc_142 : location_info := LocationInfo file_0 63 6 63 7.
+ Definition loc_143 : location_info := LocationInfo file_0 63 6 63 7.
+ Definition loc_144 : location_info := LocationInfo file_0 63 11 63 25.
(* Definition of struct [list_node]. *)
Program Definition struct_list_node := {|
@@ -176,7 +218,7 @@ Section code.
"head" <-{ LPtr }
LocInfoE loc_71 (use{LPtr} (LocInfoE loc_73 (!{LPtr} (LocInfoE loc_74 ("l"))))) ;
locinfo: loc_62 ;
- if: LocInfoE loc_62 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_62 ((LocInfoE loc_63 (use{it_layout i32} (LocInfoE loc_64 ((LocInfoE loc_65 (!{LPtr} (LocInfoE loc_67 (!{LPtr} (LocInfoE loc_68 ("l")))))) at{struct_list_node} "val")))) ≤{IntOp i32, IntOp i32} (LocInfoE loc_69 (use{it_layout i32} (LocInfoE loc_70 ("pivot")))))))
+ if: LocInfoE loc_62 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_62 ((LocInfoE loc_63 (use{it_layout i32} (LocInfoE loc_64 ("pivot")))) ≤{IntOp i32, IntOp i32} (LocInfoE loc_65 (use{it_layout i32} (LocInfoE loc_66 ((LocInfoE loc_67 (!{LPtr} (LocInfoE loc_69 (!{LPtr} (LocInfoE loc_70 ("l")))))) at{struct_list_node} "val")))))))
then
locinfo: loc_39 ;
Goto "#3"
@@ -200,4 +242,51 @@ Section code.
]> $∅
)%E
|}.
+
+ (* Definition of function [quicksort]. *)
+ Definition impl_quicksort (append partition quicksort : loc): function := {|
+ f_args := [
+ ("l", LPtr)
+ ];
+ f_local_vars := [
+ ("pivot", it_layout i32);
+ ("higher", LPtr)
+ ];
+ f_init := "#0";
+ f_code := (
+ <[ "#0" :=
+ locinfo: loc_139 ;
+ if: LocInfoE loc_139 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_139 ((LocInfoE loc_140 (use{LPtr} (LocInfoE loc_142 (!{LPtr} (LocInfoE loc_143 ("l")))))) ={PtrOp, PtrOp} (LocInfoE loc_144 (NULL)))))
+ then
+ locinfo: loc_100 ;
+ Goto "#1"
+ else
+ Goto "#2"
+ ]> $
+ <[ "#1" :=
+ locinfo: loc_100 ;
+ Return (VOID)
+ ]> $
+ <[ "#2" :=
+ "pivot" <-{ it_layout i32 }
+ LocInfoE loc_131 (use{it_layout i32} (LocInfoE loc_132 ((LocInfoE loc_133 (!{LPtr} (LocInfoE loc_135 (!{LPtr} (LocInfoE loc_136 ("l")))))) at{struct_list_node} "val"))) ;
+ locinfo: loc_122 ;
+ "$0" <- LocInfoE loc_124 (partition) with
+ [ LocInfoE loc_125 (use{LPtr} (LocInfoE loc_126 ("l"))) ;
+ LocInfoE loc_127 (use{it_layout i32} (LocInfoE loc_128 ("pivot"))) ] ;
+ "higher" <-{ LPtr } LocInfoE loc_122 ("$0") ;
+ locinfo: loc_105 ;
+ "_" <- LocInfoE loc_119 (quicksort) with
+ [ LocInfoE loc_120 (&(LocInfoE loc_121 ("higher"))) ] ;
+ locinfo: loc_106 ;
+ "_" <- LocInfoE loc_115 (quicksort) with
+ [ LocInfoE loc_116 (use{LPtr} (LocInfoE loc_117 ("l"))) ] ;
+ locinfo: loc_107 ;
+ "_" <- LocInfoE loc_109 (append) with
+ [ LocInfoE loc_110 (use{LPtr} (LocInfoE loc_111 ("l"))) ;
+ LocInfoE loc_112 (use{LPtr} (LocInfoE loc_113 ("higher"))) ] ;
+ Return (VOID)
+ ]> $∅
+ )%E
+ |}.
End code.
diff --git a/tutorial/proofs/quicksort_solution/generated_proof_append.v b/tutorial/proofs/quicksort_solution/generated_proof_append.v
index f94b8060f71a7cad51ca9515155764fd969c1704..478e520e04bef78862ab9c6907ad2c01d9c8a2ec 100644
--- a/tutorial/proofs/quicksort_solution/generated_proof_append.v
+++ b/tutorial/proofs/quicksort_solution/generated_proof_append.v
@@ -1,6 +1,7 @@
From refinedc.typing Require Import typing.
From refinedc.tutorial.quicksort_solution Require Import generated_code.
From refinedc.tutorial.quicksort_solution Require Import generated_spec.
+From refinedc.tutorial.quicksort_solution Require Import list_proofs.
Set Default Proof Using "Type".
(* Generated from [tutorial/quicksort_solution.c]. *)
diff --git a/tutorial/proofs/quicksort_solution/generated_proof_partition.v b/tutorial/proofs/quicksort_solution/generated_proof_partition.v
index 5e38bede41e902ad8c9a56ce8afbe1161f9a0355..cb59b8a90da097984b45d8b9a7286e9345721bd5 100644
--- a/tutorial/proofs/quicksort_solution/generated_proof_partition.v
+++ b/tutorial/proofs/quicksort_solution/generated_proof_partition.v
@@ -1,6 +1,7 @@
From refinedc.typing Require Import typing.
From refinedc.tutorial.quicksort_solution Require Import generated_code.
From refinedc.tutorial.quicksort_solution Require Import generated_spec.
+From refinedc.tutorial.quicksort_solution Require Import list_proofs.
Set Default Proof Using "Type".
(* Generated from [tutorial/quicksort_solution.c]. *)
diff --git a/tutorial/proofs/quicksort_solution/generated_proof_quicksort.v b/tutorial/proofs/quicksort_solution/generated_proof_quicksort.v
new file mode 100644
index 0000000000000000000000000000000000000000..919065e8da4006a9c16ede94661ce4b4a1424b75
--- /dev/null
+++ b/tutorial/proofs/quicksort_solution/generated_proof_quicksort.v
@@ -0,0 +1,31 @@
+From refinedc.typing Require Import typing.
+From refinedc.tutorial.quicksort_solution Require Import generated_code.
+From refinedc.tutorial.quicksort_solution Require Import generated_spec.
+From refinedc.tutorial.quicksort_solution Require Import list_proofs.
+Set Default Proof Using "Type".
+
+(* Generated from [tutorial/quicksort_solution.c]. *)
+Section proof_quicksort.
+ Context `{!typeG Σ} `{!globalG Σ}.
+
+ (* Typing proof for [quicksort]. *)
+ Lemma type_quicksort (append partition quicksort : loc) :
+ append â—áµ¥ append @ function_ptr type_of_append -∗
+ partition â—áµ¥ partition @ function_ptr type_of_partition -∗
+ quicksort â—áµ¥ quicksort @ function_ptr type_of_quicksort -∗
+ typed_function (impl_quicksort append partition quicksort) type_of_quicksort.
+ Proof.
+ start_function "quicksort" ([list_l l]) => arg_l local_pivot local_higher.
+ split_blocks ((
+ ∅
+ )%I : gmap label (iProp Σ)) ((
+ ∅
+ )%I : gmap label (iProp Σ)).
+ - repeat liRStep; liShow.
+ all: print_typesystem_goal "quicksort" "#0".
+ Unshelve. all: sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.
+ all: try (eapply sorted_append_middle_el => //; [ apply _ | | ]; last first).
+ all: repeat list_perm_subst; eauto using filter_permutation, Forall_filter with lia.
+ all: print_sidecondition_goal "quicksort".
+ Qed.
+End proof_quicksort.
diff --git a/tutorial/proofs/quicksort_solution/generated_spec.v b/tutorial/proofs/quicksort_solution/generated_spec.v
index 751225964bc4bd5bb88479e0ed4ec004e743971e..f83f52d2c2d39356e2dedee7dbecfc8d62fb2344 100644
--- a/tutorial/proofs/quicksort_solution/generated_spec.v
+++ b/tutorial/proofs/quicksort_solution/generated_spec.v
@@ -1,5 +1,6 @@
From refinedc.typing Require Import typing.
From refinedc.tutorial.quicksort_solution Require Import generated_code.
+From refinedc.tutorial.quicksort_solution Require Import list_proofs.
Set Default Proof Using "Type".
(* Generated from [tutorial/quicksort_solution.c]. *)
@@ -75,7 +76,12 @@ Section spec.
(* Specifications for function [partition]. *)
Definition type_of_partition :=
fn(∀ (p, xs, z) : loc * (list Z) * Z; (p @ (&own (xs @ (list_t)))), (z @ (int (i32))); True)
- → ∃ () : (), ((filter (λ v, v <= z) xs) @ (list_t)); (p â—â‚— ((filter (λ v, v > z) xs) @ (list_t))).
+ → ∃ () : (), ((filter (λ v, z <= v) xs) @ (list_t)); (p â—â‚— ((filter (λ v, v < z) xs) @ (list_t))).
+
+ (* Specifications for function [quicksort]. *)
+ Definition type_of_quicksort :=
+ fn(∀ (list_l, l) : (list Z) * loc; (l @ (&own (list_l @ (list_t)))); True)
+ → ∃ sorted_l : (list Z), (void); (l â—â‚— (sorted_l @ (list_t))) ∗ ⌜Permutation list_l sorted_l⌠∗ ⌜Sorted Z.le sorted_lâŒ.
End spec.
Typeclasses Opaque list_t_rec.
diff --git a/tutorial/proofs/quicksort_solution/list_proofs.v b/tutorial/proofs/quicksort_solution/list_proofs.v
new file mode 100644
index 0000000000000000000000000000000000000000..2eeada83e55171230bbeab42c6672c989c6573a5
--- /dev/null
+++ b/tutorial/proofs/quicksort_solution/list_proofs.v
@@ -0,0 +1,66 @@
+From refinedc.typing Require Import typing.
+Set Default Proof Using "Type".
+
+Section filter_proof.
+ Context {A : Type}.
+ Implicit Types (P : A → Prop).
+
+ Lemma filter_permutation xs P P' `{∀ x, Decision (P' x), ∀ x, Decision (P x)}:
+ (∀ x, ¬ P x ↔ P' x) →
+ xs ≡ₚ filter P xs ++ filter P' xs.
+ Proof.
+ move => HPP'.
+ induction xs as [|a xs IHxs] => //.
+ rewrite !filter_cons.
+ destruct (decide (P a)) as [HP | HnP].
+ + rewrite decide_False; [ | contradict HP; by apply HPP'].
+ apply perm_skip, IHxs.
+ + rewrite decide_True; [ | by apply HPP'].
+ rewrite -Permutation_middle.
+ apply perm_skip, IHxs.
+ Qed.
+
+ Lemma Forall_filter xs P P' `{∀ x, Decision (P' x)} :
+ (∀ x, P' x → P x) →
+ Forall P (filter P' xs).
+ Proof.
+ move => HPP'.
+ induction xs as [|a xs IHxs].
+ + by rewrite filter_nil.
+ + rewrite filter_cons.
+ destruct (decide _) => //.
+ apply Forall_cons; split => //.
+ by apply HPP'.
+ Qed.
+
+End filter_proof.
+
+Section sorted_list_proof.
+ Context {A : Type}.
+ Context (R : A → A → Prop).
+
+ Lemma sorted_append_middle_el xs ys m:
+ Transitive R →
+ Sorted R xs →
+ Sorted R ys →
+ Forall (λ e, R e m) xs →
+ Forall (λ e, R m e) ys →
+ Sorted R (xs ++ ys).
+ Proof.
+ move => H /Sorted_StronglySorted H1 /Sorted_StronglySorted H2 Hxs Hys.
+ apply StronglySorted_Sorted.
+ induction xs as [|a xs IHxs] => //=.
+ inversion Hxs. apply SSorted_cons.
+ + apply: IHxs => //.
+ by eapply StronglySorted_inv.
+ + apply Forall_app_2; first by apply StronglySorted_inv.
+ eapply Forall_impl => //= x3.
+ by apply H.
+ Qed.
+
+End sorted_list_proof.
+
+Ltac list_perm_subst :=
+ match goal with
+ | H: ?listL ≡ₚ ?listR |- ?P => (rewrite H => {H} || rewrite -H => {H})
+ end.
diff --git a/tutorial/proofs/quicksort_solution/proof_files b/tutorial/proofs/quicksort_solution/proof_files
index 0b5500e1fa751b051c84d9e1dec5cfc16c444de8..97f3be09afdc26dbbbdfcfaddd45eb4b45e1b45c 100644
--- a/tutorial/proofs/quicksort_solution/proof_files
+++ b/tutorial/proofs/quicksort_solution/proof_files
@@ -1,2 +1,3 @@
generated_proof_append.v
generated_proof_partition.v
+generated_proof_quicksort.v
diff --git a/tutorial/quicksort_exercise.c b/tutorial/quicksort_exercise.c
index cf41841a757bc2676480e4fc389633d18aaf49c6..1ee5e52468b546912363145ee75d75db6c4ece9d 100644
--- a/tutorial/quicksort_exercise.c
+++ b/tutorial/quicksort_exercise.c
@@ -32,7 +32,7 @@ list_t partition(list_t *l, int pivot) {
} else {
list_t rest = partition(&(*l)->next, pivot);
list_t head = *l;
- if((*l)->val <= pivot) {
+ if(pivot <= (*l)->val) {
*l = (*l)->next;
head->next = rest;
return head;
@@ -41,3 +41,15 @@ list_t partition(list_t *l, int pivot) {
}
}
}
+
+void quicksort(list_t* l) {
+ if(*l == NULL) {
+ return;
+ } else {
+ int pivot = (*l)->val;
+ list_t higher = partition(l, pivot);
+ quicksort(&higher);
+ quicksort(l);
+ append(l, higher);
+ }
+}
diff --git a/tutorial/quicksort_solution.c b/tutorial/quicksort_solution.c
index 6b3918f18143a756804b10089ddbfda46a065086..65c848de2108bd2837a8622c28b4fbcb815b4b04 100644
--- a/tutorial/quicksort_solution.c
+++ b/tutorial/quicksort_solution.c
@@ -1,5 +1,7 @@
#include <stddef.h>
+//@rc::import list_proofs from refinedc.tutorial.quicksort_solution
+
typedef struct
[[rc::refined_by("xs : {list Z}")]]
[[rc::ptr_type("list_t : {xs <> []} @ optional<&own<...>, null>")]]
@@ -32,8 +34,8 @@ void append(list_t *l, list_t k) {
[[rc::parameters("p : loc", "xs : {list Z}", "z : Z")]]
[[rc::args("p @ &own<xs @ list_t>", "z @ int<i32>")]]
-[[rc::returns("{filter (λ v, v <= z) xs} @ list_t")]]
-[[rc::ensures("p @ &own<{filter (λ v, v > z) xs} @ list_t>")]]
+[[rc::returns("{filter (λ v, z <= v) xs} @ list_t")]]
+[[rc::ensures("p @ &own<{filter (λ v, v < z) xs} @ list_t>")]]
[[rc::tactics("all: try by rewrite filter_cons; solve_goal.")]]
list_t partition(list_t *l, int pivot) {
if(*l == NULL) {
@@ -41,7 +43,7 @@ list_t partition(list_t *l, int pivot) {
} else {
list_t rest = partition(&(*l)->next, pivot);
list_t head = *l;
- if((*l)->val <= pivot) {
+ if(pivot <= (*l)->val) {
*l = (*l)->next;
head->next = rest;
return head;
@@ -51,4 +53,20 @@ list_t partition(list_t *l, int pivot) {
}
}
-// TODO: quicksort
+[[rc::parameters ("list_l : {list Z}", "l : loc")]]
+[[rc::args ("l @ &own<list_l @ list_t>")]]
+[[rc::exists ("sorted_l : {list Z}")]]
+[[rc::ensures ("l @ &own<sorted_l @ list_t>", "{Permutation list_l sorted_l}", "{Sorted Z.le sorted_l}")]]
+[[rc::tactics ("all: try (eapply sorted_append_middle_el => //; [ apply _ | | ]; last first).")]]
+[[rc::tactics ("all: repeat list_perm_subst; eauto using filter_permutation, Forall_filter with lia.")]]
+void quicksort(list_t* l) {
+ if(*l == NULL) {
+ return;
+ } else {
+ int pivot = (*l)->val;
+ list_t higher = partition(l, pivot);
+ quicksort(&higher);
+ quicksort(l);
+ append(l, higher);
+ }
+}