Example with tagged pointers.

_CoqProject

@@ -50,3 +50,4 @@
 -Q _build/default/linux/proofs/early_alloc_simplified refinedc.linux.early_alloc_simplified
 -Q _build/default/linux/casestudies/proofs/early_alloc refinedc.linux.casestudies.early_alloc
 -Q _build/default/examples/proofs/quick_sort refinedc.examples.quick_sort
+-Q _build/default/examples/proofs/tagged_ptr refinedc.examples.tagged_ptr

examples/proofs/tagged_ptr/dune

+; Generated by [refinedc], do not edit.
+(coq.theory
+ (flags -w -notation-overridden -w -redundant-canonical-projection)
+ (name refinedc.examples.tagged_ptr)
+ (theories refinedc.lang refinedc.lithium refinedc.typing refinedc.typing.automation))

examples/proofs/tagged_ptr/generated_code.v

+From refinedc.lang Require Export notation.
+From refinedc.lang Require Import tactics.
+From refinedc.typing Require Import annotations.
+Set Default Proof Using "Type".
+
+(* Generated from [examples/tagged_ptr.c]. *)
+Section code.
+  Definition file_0 : string := "examples/tagged_ptr.c".
+  Definition loc_2 : location_info := LocationInfo file_0 20 2 20 36.
+  Definition loc_3 : location_info := LocationInfo file_0 20 9 20 35.
+  Definition loc_4 : location_info := LocationInfo file_0 20 9 20 24.
+  Definition loc_5 : location_info := LocationInfo file_0 20 22 20 23.
+  Definition loc_6 : location_info := LocationInfo file_0 20 22 20 23.
+  Definition loc_7 : location_info := LocationInfo file_0 20 27 20 35.
+  Definition loc_8 : location_info := LocationInfo file_0 20 28 20 29.
+  Definition loc_9 : location_info := LocationInfo file_0 20 33 20 34.
+  Definition loc_12 : location_info := LocationInfo file_0 28 2 28 26.
+  Definition loc_13 : location_info := LocationInfo file_0 29 2 29 139.
+  Definition loc_14 : location_info := LocationInfo file_0 29 9 29 138.
+  Definition loc_15 : location_info := LocationInfo file_0 29 35 29 38.
+  Definition loc_16 : location_info := LocationInfo file_0 29 35 29 38.
+  Definition loc_17 : location_info := LocationInfo file_0 29 40 29 77.
+  Definition loc_18 : location_info := LocationInfo file_0 29 49 29 76.
+  Definition loc_19 : location_info := LocationInfo file_0 29 50 29 71.
+  Definition loc_20 : location_info := LocationInfo file_0 29 50 29 63.
+  Definition loc_21 : location_info := LocationInfo file_0 29 62 29 63.
+  Definition loc_22 : location_info := LocationInfo file_0 29 62 29 63.
+  Definition loc_23 : location_info := LocationInfo file_0 29 66 29 71.
+  Definition loc_24 : location_info := LocationInfo file_0 29 66 29 71.
+  Definition loc_25 : location_info := LocationInfo file_0 29 74 29 75.
+  Definition loc_26 : location_info := LocationInfo file_0 29 74 29 75.
+  Definition loc_27 : location_info := LocationInfo file_0 28 16 28 25.
+  Definition loc_28 : location_info := LocationInfo file_0 28 16 28 22.
+  Definition loc_29 : location_info := LocationInfo file_0 28 16 28 22.
+  Definition loc_30 : location_info := LocationInfo file_0 28 23 28 24.
+  Definition loc_31 : location_info := LocationInfo file_0 28 23 28 24.
+  Definition loc_36 : location_info := LocationInfo file_0 36 2 36 30.
+  Definition loc_37 : location_info := LocationInfo file_0 37 2 37 121.
+  Definition loc_38 : location_info := LocationInfo file_0 37 9 37 120.
+  Definition loc_39 : location_info := LocationInfo file_0 37 35 37 38.
+  Definition loc_40 : location_info := LocationInfo file_0 37 35 37 38.
+  Definition loc_41 : location_info := LocationInfo file_0 37 40 37 68.
+  Definition loc_42 : location_info := LocationInfo file_0 37 49 37 67.
+  Definition loc_43 : location_info := LocationInfo file_0 37 50 37 51.
+  Definition loc_44 : location_info := LocationInfo file_0 37 50 37 51.
+  Definition loc_45 : location_info := LocationInfo file_0 37 54 37 66.
+  Definition loc_46 : location_info := LocationInfo file_0 37 54 37 55.
+  Definition loc_47 : location_info := LocationInfo file_0 37 54 37 55.
+  Definition loc_48 : location_info := LocationInfo file_0 37 58 37 66.
+  Definition loc_49 : location_info := LocationInfo file_0 37 59 37 60.
+  Definition loc_50 : location_info := LocationInfo file_0 37 64 37 65.
+  Definition loc_51 : location_info := LocationInfo file_0 36 16 36 29.
+  Definition loc_52 : location_info := LocationInfo file_0 36 28 36 29.
+  Definition loc_53 : location_info := LocationInfo file_0 36 28 36 29.
+  Definition loc_58 : location_info := LocationInfo file_0 42 2 42 15.
+  Definition loc_59 : location_info := LocationInfo file_0 44 2 44 24.
+  Definition loc_60 : location_info := LocationInfo file_0 45 2 45 26.
+  Definition loc_61 : location_info := LocationInfo file_0 47 2 47 36.
+  Definition loc_62 : location_info := LocationInfo file_0 48 2 48 13.
+  Definition loc_63 : location_info := LocationInfo file_0 48 9 48 12.
+  Definition loc_64 : location_info := LocationInfo file_0 48 9 48 12.
+  Definition loc_65 : location_info := LocationInfo file_0 48 10 48 12.
+  Definition loc_66 : location_info := LocationInfo file_0 48 10 48 12.
+  Definition loc_67 : location_info := LocationInfo file_0 47 15 47 35.
+  Definition loc_68 : location_info := LocationInfo file_0 47 26 47 35.
+  Definition loc_69 : location_info := LocationInfo file_0 47 26 47 31.
+  Definition loc_70 : location_info := LocationInfo file_0 47 26 47 31.
+  Definition loc_71 : location_info := LocationInfo file_0 47 32 47 34.
+  Definition loc_72 : location_info := LocationInfo file_0 47 32 47 34.
+  Definition loc_75 : location_info := LocationInfo file_0 45 9 45 24.
+  Definition loc_76 : location_info := LocationInfo file_0 45 9 45 19.
+  Definition loc_77 : location_info := LocationInfo file_0 45 9 45 15.
+  Definition loc_78 : location_info := LocationInfo file_0 45 9 45 15.
+  Definition loc_79 : location_info := LocationInfo file_0 45 16 45 18.
+  Definition loc_80 : location_info := LocationInfo file_0 45 16 45 18.
+  Definition loc_81 : location_info := LocationInfo file_0 45 23 45 24.
+  Definition loc_82 : location_info := LocationInfo file_0 44 13 44 23.
+  Definition loc_83 : location_info := LocationInfo file_0 44 13 44 16.
+  Definition loc_84 : location_info := LocationInfo file_0 44 13 44 16.
+  Definition loc_85 : location_info := LocationInfo file_0 44 17 44 19.
+  Definition loc_86 : location_info := LocationInfo file_0 44 18 44 19.
+  Definition loc_87 : location_info := LocationInfo file_0 44 21 44 22.
+  Definition loc_90 : location_info := LocationInfo file_0 42 13 42 14.
+  Definition loc_95 : location_info := LocationInfo file_0 57 2 57 30.
+  Definition loc_96 : location_info := LocationInfo file_0 58 2 58 27.
+  Definition loc_97 : location_info := LocationInfo file_0 58 9 58 26.
+  Definition loc_98 : location_info := LocationInfo file_0 58 9 58 21.
+  Definition loc_99 : location_info := LocationInfo file_0 58 9 58 10.
+  Definition loc_100 : location_info := LocationInfo file_0 58 9 58 10.
+  Definition loc_101 : location_info := LocationInfo file_0 58 13 58 21.
+  Definition loc_102 : location_info := LocationInfo file_0 58 14 58 15.
+  Definition loc_103 : location_info := LocationInfo file_0 58 19 58 20.
+  Definition loc_104 : location_info := LocationInfo file_0 58 25 58 26.
+  Definition loc_105 : location_info := LocationInfo file_0 57 16 57 29.
+  Definition loc_106 : location_info := LocationInfo file_0 57 28 57 29.
+  Definition loc_107 : location_info := LocationInfo file_0 57 28 57 29.
+
+  (* Definition of function [tag_of]. *)
+  Definition impl_tag_of : function := {|
+    f_args := [
+      ("p", void*)
+    ];
+    f_local_vars := [
+    ];
+    f_init := "#0";
+    f_code := (
+      <[ "#0" :=
+        locinfo: loc_2 ;
+        Return (LocInfoE loc_3 (UnOp (CastOp $ IntOp u8) (IntOp uintptr_t) (LocInfoE loc_3 ((LocInfoE loc_4 (UnOp (CastOp $ IntOp uintptr_t) (PtrOp) (LocInfoE loc_5 (use{void*} (LocInfoE loc_6 ("p")))))) %{IntOp uintptr_t, IntOp uintptr_t} (LocInfoE loc_7 (UnOp (CastOp $ IntOp uintptr_t) (IntOp i32) (LocInfoE loc_7 ((LocInfoE loc_8 (i2v 1 i32)) <<{IntOp i32, IntOp i32} (LocInfoE loc_9 (i2v 3 i32))))))))))
+      ]> $∅
+    )%E
+  |}.
+
+  (* Definition of function [tag]. *)
+  Definition impl_tag (global_tag_of : loc): function := {|
+    f_args := [
+      ("p", void*);
+      ("t", it_layout u8)
+    ];
+    f_local_vars := [
+      ("old_t", it_layout u8)
+    ];
+    f_init := "#0";
+    f_code := (
+      <[ "#0" :=
+        "old_t" <-{ it_layout u8 }
+          LocInfoE loc_27 (Call (LocInfoE loc_29 (global_tag_of)) [@{expr} LocInfoE loc_30 (use{void*} (LocInfoE loc_31 ("p"))) ]) ;
+        locinfo: loc_13 ;
+        Return (LocInfoE loc_14 (CopyAllocId (PtrOp) (LocInfoE loc_17 (UnOp (CastOp $ PtrOp) (IntOp uintptr_t) (LocInfoE loc_18 ((LocInfoE loc_19 ((LocInfoE loc_20 (UnOp (CastOp $ IntOp uintptr_t) (PtrOp) (LocInfoE loc_21 (use{void*} (LocInfoE loc_22 ("p")))))) -{IntOp uintptr_t, IntOp uintptr_t} (LocInfoE loc_23 (UnOp (CastOp $ IntOp uintptr_t) (IntOp u8) (LocInfoE loc_23 (use{it_layout u8} (LocInfoE loc_24 ("old_t")))))))) +{IntOp uintptr_t, IntOp uintptr_t} (LocInfoE loc_25 (UnOp (CastOp $ IntOp uintptr_t) (IntOp u8) (LocInfoE loc_25 (use{it_layout u8} (LocInfoE loc_26 ("t")))))))))) (LocInfoE loc_15 (use{void*} (LocInfoE loc_16 ("p"))))))
+      ]> $∅
+    )%E
+  |}.
+
+  (* Definition of function [untag]. *)
+  Definition impl_untag : function := {|
+    f_args := [
+      ("p", void*)
+    ];
+    f_local_vars := [
+      ("i", it_layout uintptr_t)
+    ];
+    f_init := "#0";
+    f_code := (
+      <[ "#0" :=
+        "i" <-{ it_layout uintptr_t }
+          LocInfoE loc_51 (UnOp (CastOp $ IntOp uintptr_t) (PtrOp) (LocInfoE loc_52 (use{void*} (LocInfoE loc_53 ("p"))))) ;
+        locinfo: loc_37 ;
+        Return (LocInfoE loc_38 (CopyAllocId (PtrOp) (LocInfoE loc_41 (UnOp (CastOp $ PtrOp) (IntOp uintptr_t) (LocInfoE loc_42 ((LocInfoE loc_43 (use{it_layout uintptr_t} (LocInfoE loc_44 ("i")))) -{IntOp uintptr_t, IntOp uintptr_t} (LocInfoE loc_45 ((LocInfoE loc_46 (use{it_layout uintptr_t} (LocInfoE loc_47 ("i")))) %{IntOp uintptr_t, IntOp uintptr_t} (LocInfoE loc_48 (UnOp (CastOp $ IntOp uintptr_t) (IntOp i32) (LocInfoE loc_48 ((LocInfoE loc_49 (i2v 1 i32)) <<{IntOp i32, IntOp i32} (LocInfoE loc_50 (i2v 3 i32)))))))))))) (LocInfoE loc_39 (use{void*} (LocInfoE loc_40 ("p"))))))
+      ]> $∅
+    )%E
+  |}.
+
+  (* Definition of function [test]. *)
+  Definition impl_test (global_tag global_tag_of global_untag : loc): function := {|
+    f_args := [
+    ];
+    f_local_vars := [
+      ("tp", void*);
+      ("x", it_layout size_t);
+      ("px", void*)
+    ];
+    f_init := "#0";
+    f_code := (
+      <[ "#0" :=
+        "x" <-{ it_layout size_t }
+          LocInfoE loc_90 (UnOp (CastOp $ IntOp size_t) (IntOp i32) (LocInfoE loc_90 (i2v 0 i32))) ;
+        "tp" <-{ void* }
+          LocInfoE loc_82 (Call (LocInfoE loc_84 (global_tag)) [@{expr} LocInfoE loc_85 (&(LocInfoE loc_86 ("x"))) ;
+          LocInfoE loc_87 (UnOp (CastOp $ IntOp u8) (IntOp i32) (LocInfoE loc_87 (i2v 1 i32))) ]) ;
+        locinfo: loc_60 ;
+        assert: (LocInfoE loc_75 (UnOp (CastOp $ IntOp bool_it) (IntOp i32) (LocInfoE loc_75 ((LocInfoE loc_76 (UnOp (CastOp $ IntOp i32) (IntOp u8) (LocInfoE loc_76 (Call (LocInfoE loc_78 (global_tag_of)) [@{expr} LocInfoE loc_79 (use{void*} (LocInfoE loc_80 ("tp"))) ])))) ={IntOp i32, IntOp i32} (LocInfoE loc_81 (i2v 1 i32)))))) ;
+        "px" <-{ void* }
+          LocInfoE loc_67 (UnOp (CastOp $ PtrOp) (PtrOp) (LocInfoE loc_68 (Call (LocInfoE loc_70 (global_untag)) [@{expr} LocInfoE loc_71 (use{void*} (LocInfoE loc_72 ("tp"))) ]))) ;
+        locinfo: loc_62 ;
+        Return (LocInfoE loc_63 (use{it_layout size_t} (LocInfoE loc_65 (!{void*} (LocInfoE loc_66 ("px"))))))
+      ]> $∅
+    )%E
+  |}.
+
+  (* Definition of function [is_aligned]. *)
+  Definition impl_is_aligned : function := {|
+    f_args := [
+      ("p", void*)
+    ];
+    f_local_vars := [
+      ("i", it_layout uintptr_t)
+    ];
+    f_init := "#0";
+    f_code := (
+      <[ "#0" :=
+        "i" <-{ it_layout uintptr_t }
+          LocInfoE loc_105 (UnOp (CastOp $ IntOp uintptr_t) (PtrOp) (LocInfoE loc_106 (use{void*} (LocInfoE loc_107 ("p"))))) ;
+        locinfo: loc_96 ;
+        Return (LocInfoE loc_97 ((LocInfoE loc_98 ((LocInfoE loc_99 (use{it_layout uintptr_t} (LocInfoE loc_100 ("i")))) %{IntOp uintptr_t, IntOp uintptr_t} (LocInfoE loc_101 (UnOp (CastOp $ IntOp uintptr_t) (IntOp i32) (LocInfoE loc_101 ((LocInfoE loc_102 (i2v 1 i32)) <<{IntOp i32, IntOp i32} (LocInfoE loc_103 (i2v 3 i32)))))))) ={IntOp uintptr_t, IntOp uintptr_t} (LocInfoE loc_104 (UnOp (CastOp $ IntOp uintptr_t) (IntOp i32) (LocInfoE loc_104 (i2v 0 i32))))))
+      ]> $∅
+    )%E
+  |}.
+End code.

examples/proofs/tagged_ptr/generated_proof_is_aligned.v

+From refinedc.typing Require Import typing.
+From refinedc.examples.tagged_ptr Require Import generated_code.
+From refinedc.examples.tagged_ptr Require Import generated_spec.
+Set Default Proof Using "Type".
+
+(* Generated from [examples/tagged_ptr.c]. *)
+Section proof_is_aligned.
+  Context `{!typeG Σ} `{!globalG Σ}.
+
+  (* Typing proof for [is_aligned]. *)
+  Lemma type_is_aligned :
+    ⊢ typed_function impl_is_aligned type_of_is_aligned.
+  Proof.
+    Open Scope printing_sugar.
+    start_function "is_aligned" ([[l beta] n]) => arg_p local_i.
+    split_blocks ((
+      ∅
+    )%I : gmap label (iProp Σ)) ((
+      ∅
+    )%I : gmap label (iProp Σ)).
+    - repeat liRStep; liShow.
+      all: print_typesystem_goal "is_aligned" "#0".
+    Unshelve. all: sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.
+    all: unfold aligned_to in *; split; solve_goal.
+    all: print_sidecondition_goal "is_aligned".
+  Qed.
+End proof_is_aligned.

examples/proofs/tagged_ptr/generated_proof_tag.v

+From refinedc.typing Require Import typing.
+From refinedc.examples.tagged_ptr Require Import generated_code.
+From refinedc.examples.tagged_ptr Require Import generated_spec.
+Set Default Proof Using "Type".
+
+(* Generated from [examples/tagged_ptr.c]. *)
+Section proof_tag.
+  Context `{!typeG Σ} `{!globalG Σ}.
+
+  (* Typing proof for [tag]. *)
+  Lemma type_tag (global_tag_of : loc) :
+    global_tag_of ◁ᵥ global_tag_of @ function_ptr type_of_tag_of -∗
+    typed_function (impl_tag global_tag_of) type_of_tag.
+  Proof.
+    Open Scope printing_sugar.
+    start_function "tag" ([[r t] ty]) => arg_p arg_t local_old_t.
+    split_blocks ((
+      ∅
+    )%I : gmap label (iProp Σ)) ((
+      ∅
+    )%I : gmap label (iProp Σ)).
+    - repeat liRStep; liShow.
+      all: print_typesystem_goal "tag" "#0".
+    Unshelve. all: sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.
+    all: print_sidecondition_goal "tag".
+  Qed.
+End proof_tag.

examples/proofs/tagged_ptr/generated_proof_tag_of.v

+From refinedc.typing Require Import typing.
+From refinedc.examples.tagged_ptr Require Import generated_code.
+From refinedc.examples.tagged_ptr Require Import generated_spec.
+Set Default Proof Using "Type".
+
+(* Generated from [examples/tagged_ptr.c]. *)
+Section proof_tag_of.
+  Context `{!typeG Σ} `{!globalG Σ}.
+
+  (* Typing proof for [tag_of]. *)
+  Lemma type_tag_of :
+    ⊢ typed_function impl_tag_of type_of_tag_of.
+  Proof.
+    Open Scope printing_sugar.
+    start_function "tag_of" ([[r ty] v]) => arg_p.
+    split_blocks ((
+      ∅
+    )%I : gmap label (iProp Σ)) ((
+      ∅
+    )%I : gmap label (iProp Σ)).
+    - repeat liRStep; liShow.
+      all: print_typesystem_goal "tag_of" "#0".
+    Unshelve. all: sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.
+    all: print_sidecondition_goal "tag_of".
+  Qed.
+End proof_tag_of.

examples/proofs/tagged_ptr/generated_proof_test.v

+From refinedc.typing Require Import typing.
+From refinedc.examples.tagged_ptr Require Import generated_code.
+From refinedc.examples.tagged_ptr Require Import generated_spec.
+Set Default Proof Using "Type".
+
+(* Generated from [examples/tagged_ptr.c]. *)
+Section proof_test.
+  Context `{!typeG Σ} `{!globalG Σ}.
+
+  (* Typing proof for [test]. *)
+  Lemma type_test (global_tag global_tag_of global_untag : loc) :
+    global_tag ◁ᵥ global_tag @ function_ptr type_of_tag -∗
+    global_tag_of ◁ᵥ global_tag_of @ function_ptr type_of_tag_of -∗
+    global_untag ◁ᵥ global_untag @ function_ptr type_of_untag -∗
+    typed_function (impl_test global_tag global_tag_of global_untag) type_of_test.
+  Proof.
+    Open Scope printing_sugar.
+    start_function "test" ([]) => local_tp local_x local_px.
+    split_blocks ((
+      ∅
+    )%I : gmap label (iProp Σ)) ((
+      ∅
+    )%I : gmap label (iProp Σ)).
+    - repeat liRStep; liShow.
+      all: print_typesystem_goal "test" "#0".
+    Unshelve. all: sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.
+    all: print_sidecondition_goal "test".
+  Qed.
+End proof_test.

examples/proofs/tagged_ptr/generated_proof_untag.v

+From refinedc.typing Require Import typing.
+From refinedc.examples.tagged_ptr Require Import generated_code.
+From refinedc.examples.tagged_ptr Require Import generated_spec.
+Set Default Proof Using "Type".
+
+(* Generated from [examples/tagged_ptr.c]. *)
+Section proof_untag.
+  Context `{!typeG Σ} `{!globalG Σ}.
+
+  (* Typing proof for [untag]. *)
+  Lemma type_untag :
+    ⊢ typed_function impl_untag type_of_untag.
+  Proof.
+    Open Scope printing_sugar.
+    start_function "untag" ([r ty]) => arg_p local_i.
+    split_blocks ((
+      ∅
+    )%I : gmap label (iProp Σ)) ((
+      ∅
+    )%I : gmap label (iProp Σ)).
+    - repeat liRStep; liShow.
+      all: print_typesystem_goal "untag" "#0".
+    Unshelve. all: sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.
+    all: print_sidecondition_goal "untag".
+  Qed.
+End proof_untag.

examples/proofs/tagged_ptr/generated_spec.v

+From refinedc.typing Require Import typing.
+From refinedc.examples.tagged_ptr Require Import generated_code.
+Set Default Proof Using "Type".
+
+(* Generated from [examples/tagged_ptr.c]. *)
+Section spec.
+  Context `{!typeG Σ} `{!globalG Σ}.
+
+  (* Inlined code. *)
+
+  Notation TAG_MOD := (8%nat) (only parsing).
+
+  (* Type definitions. *)
+
+  (* Specifications for function [tag_of]. *)
+  Definition type_of_tag_of :=
+    fn(∀ (r, ty, v) : (loc * Z) * type * val; (value (void*) (v)); (v ◁ᵥ (r @ (tagged_ptr (Own) (TAG_MOD) (ty)))))
+      → ∃ () : (), ((r.2) @ (int (u8))); ⌜0 ≤ r.2 < TAG_MOD⌝ ∗ (v ◁ᵥ (r @ (tagged_ptr (Own) (TAG_MOD) (ty)))).
+
+  (* Specifications for function [tag]. *)
+  Definition type_of_tag :=
+    fn(∀ (r, t, ty) : (loc * Z) * Z * type; (r @ (tagged_ptr (Own) (TAG_MOD) (ty))), (t @ (int (u8))); ⌜0 ≤ t < TAG_MOD⌝)
+      → ∃ () : (), (((r.1, t)) @ (tagged_ptr (Own) (TAG_MOD) (ty))); True.
+
+  (* Specifications for function [untag]. *)
+  Definition type_of_untag :=
+    fn(∀ (r, ty) : (loc * Z) * type; (r @ (tagged_ptr (Own) (TAG_MOD) (ty))); True)
+      → ∃ () : (), ((r.1) @ (&own (ty))); True.
+
+  (* Specifications for function [test]. *)
+  Definition type_of_test :=
+    fn(∀ () : (); True) → ∃ () : (), ((0) @ (int (size_t))); True.
+
+  (* Specifications for function [is_aligned]. *)
+  Definition type_of_is_aligned :=
+    fn(∀ (l, beta, n) : loc * own_state * Z; (l @ (&frac{beta} (n @ (int (i32))))); True)
+      → ∃ () : (), ((bool_decide (l `aligned_to` 8%nat)) @ (boolean (i32))); (l ◁ₗ{beta} (n @ (int (i32)))).
+End spec.

examples/proofs/tagged_ptr/proof_files

+generated_proof_is_aligned.v
+generated_proof_tag.v
+generated_proof_tag_of.v
+generated_proof_test.v
+generated_proof_untag.v

examples/tagged_ptr.c

+#include <stddef.h>
+#include <stdint.h>
+#include <refinedc.h>
+
+#define TAG_SIZE 3
+#define TAG_MOD  (1 << TAG_SIZE)
+#define TAG_MASK (TAG_MOD - 1)
+
+typedef unsigned char tag_t;
+
+//@rc::inlined Notation TAG_MOD := (8%nat) (only parsing).
+
+[[rc::parameters("r: {loc * Z}", "ty : type", "v : val")]]
+[[rc::args("value<void*, v>")]]
+[[rc::requires("v : r @ tagged_ptr<Own, TAG_MOD, ty>")]]
+[[rc::returns("{r.2} @ int<u8>")]]
+[[rc::ensures("{0 ≤ r.2 < TAG_MOD}")]]
+[[rc::ensures("v : r @ tagged_ptr<Own, TAG_MOD, ty>")]]
+tag_t tag_of(void* p){
+  return ((uintptr_t) p) % TAG_MOD;
+}
+
+[[rc::parameters("r: {loc * Z}", "t: Z", "ty: type")]]
+[[rc::args("r @ tagged_ptr<Own, TAG_MOD, ty>", "t @ int<u8>")]]
+[[rc::requires("{0 ≤ t < TAG_MOD}")]]
+[[rc::returns("{(r.1, t)} @ tagged_ptr<Own, TAG_MOD, ty>")]]
+void* tag(void* p, tag_t t){
+  tag_t old_t = tag_of(p);
+  return rc_copy_alloc_id((void*) ((uintptr_t) p - old_t + t), p);
+}
+
+[[rc::parameters("r: {loc * Z}", "ty: type")]]
+[[rc::args("r @ tagged_ptr<Own, TAG_MOD, ty>")]]
+[[rc::returns("{r.1} @ &own<ty>")]]
+void* untag(void* p){
+  uintptr_t i = (uintptr_t) p;
+  return rc_copy_alloc_id((void*) (i - i % TAG_MOD), p);
+}
+
+[[rc::returns("{0} @ int<size_t>")]]
+size_t test(){
+  size_t x = 0;
+
+  void *tp = tag(&x, 1);
+  assert(tag_of(tp) == 1);
+
+  size_t *px = (size_t *) untag(tp);
+  return *px;
+}
+
+[[rc::parameters("l: loc", "beta: own_state", "n: Z")]]
+[[rc::args("l @ &frac<beta, n @ int<i32>>")]]
+[[rc::returns("{bool_decide (l `aligned_to` 8%nat)} @ boolean<i32>")]]
+[[rc::ensures("frac beta l : n @ int<i32>")]]
+[[rc::tactics("all: unfold aligned_to in *; split; solve_goal.")]]
+int is_aligned(void* p){
+  uintptr_t i = (uintptr_t) p;
+  return i % TAG_MOD == 0;
+}

theories/lang/loc.v

@@ -155,3 +155,6 @@ Proof.
   unfold aligned_to. destruct l => /= ??. apply: Z.divide_add_cancel_r => //.
   apply: (Zdivide_mult_l _ n1). by rewrite Z.mul_comm -Nat2Z.inj_mul.
 Qed.
+
+Instance aligned_to_dec l n : Decision (l `aligned_to` n).
+Proof. apply Znumtheory.Zdivide_dec. Qed.

theories/lang/notation.v

@@ -55,16 +55,17 @@ Notation "e1 'at_neg_offset{' ly , ot1 , ot2 } e2" := (BinOp (PtrNegOffsetOp ly)
   (at level 70, format "e1  at_neg_offset{ ly ,  ot1 ,  ot2 }  e2") : expr_scope.
 (* The unicode ← is already part of the notation "_ ← _; _" for bind. *)
 Notation "e1 <-{ ly , o } e2 ; s" := (Assign o ly e1%E e2%E s%E)
-  (at level 80, s at level 200, format "e1  <-{ ly ,  o }  e2 ;  s") : expr_scope.
+  (at level 80, s at level 200, format "'[v' e1  '<-{' ly ',' o '}'  e2 ';' '/' s ']'") : expr_scope.
 Notation "e1 <-{ ly } e2 ; s" := (Assign Na1Ord ly e1%E e2%E s%E)
-  (at level 80, s at level 200, format "e1  <-{ ly }  e2 ;  s") : expr_scope.
+  (at level 80, s at level 200, format "'[v' e1  '<-{' ly '}'  e2 ';' '/' s ']'") : expr_scope.
 Notation "'if:' e1 'then' s1 'else' s2" := (Switch bool_it e1%E {[ 0 := 0%nat ]} [s2%E] s1%E)
-  (at level 102, e1, s1, s2 at level 150) : expr_scope.
+  (at level 102, e1, s1, s2 at level 150, format "'[v' 'if:'  e1  'then' '/  ' s1 '/' 'else' '/  ' s2 ']'") : expr_scope.
 Notation "'expr:' e ; s" := (ExprS e%E s%E)
-  (at level 80, s at level 200, format "'expr:'  e ;  s") : expr_scope.
+  (at level 80, s at level 200, format "'[v' 'expr:'  e ';' '/' s ']'") : expr_scope.
 
 Definition Assert (e : expr) (s : stmt) : stmt := (if: e then s else StuckS)%E.
-Notation "'assert:' e ; s" := (Assert e%E s%E) (at level 80, s at level 200, format "'assert:'  e ;  s") : expr_scope.
+Notation "'assert:' e ; s" := (Assert e%E s%E)
+  (at level 80, s at level 200, format "'[v' 'assert:'  e ';' '/' s ']'") : expr_scope.
 Arguments Assert : simpl never.
 Typeclasses Opaque Assert.
 
@@ -100,7 +101,7 @@ Definition LocInfo {B} (a : location_info) (b : B) := b.
 Arguments LocInfo : simpl never.
 Typeclasses Opaque LocInfo.
 Notation "'locinfo:' a ; b" := (LocInfo (B:=stmt) a b%E)
-  (at level 80, b at level 200, format "'locinfo:'  a ;  b") : expr_scope.
+  (at level 80, b at level 200, format "'[v' 'locinfo:'  a ';' '/' b ']'") : expr_scope.
 Notation LocInfoE := (LocInfo (B:=expr)).
 
 Definition MacroE (m : list expr → expr) (es : list expr) := m es.

theories/lithium/base.v

@@ -62,6 +62,32 @@ Tactic Notation "reduce_closed" constr(x) :=
   change_no_check x with r in *
 .
 
+(*
+The following tactics are currently not used.
+
+(* TODO: This tactic is quite inefficient (it calls unification for
+every subterm in the goal and hyps). Can we do something about this? *)
+Tactic Notation "select" "subterm" open_constr(pat) tactic3(tac) :=
+  match goal with
+  | |- context H [?x]       => unify x pat; tac x
+  | _ : context H [?x] |- _ => unify x pat; tac x
+  end.
+
+Tactic Notation "reduce" "pattern" open_constr(pat) :=
+  repeat select subterm pat (fun x => reduce_closed x).
+
+(* TODO: This tactic is quite inefficient (it calls unification for
+every subterm in the goal and hyps). Can we do something about this? *)
+Tactic Notation "select" "closed" "subterm" "of" "type" constr(T) tactic3(tac) :=
+  match goal with
+  | |- context H [?x]       => let ty := type of x in unify ty T; check_closed x; tac x
+  | _ : context H