chore(na): Move test examples into own file

theories/rust_typing/existentials_na_test.v

+(* NOTE: This file is expected to be deleted when the `rr_frontend` will be done. *)
+
+From refinedrust Require Import automation.
+From refinedrust Require Import existentials_na.
+From refinedrust Require Import typing.
+
+Section UnsafeCell_sls.
+  Context `{!refinedrustGS Σ}.
+
+  Definition UnsafeCell_sls : struct_layout_spec := mk_sls "UnsafeCell" [
+    ("value", IntSynType I32)] StructReprTransparent.
+  Definition UnsafeCell_st : syn_type := UnsafeCell_sls.
+End UnsafeCell_sls.
+
+Section Cell_sls.
+  Context `{!refinedrustGS Σ}.
+
+  Definition Cell_sls  : struct_layout_spec := mk_sls "Cell" [
+    ("value", UnsafeCell_st)] StructReprRust.
+  Definition Cell_st  : syn_type := Cell_sls .
+End Cell_sls.
+
+Section code.
+  Context `{!refinedrustGS Σ}.
+  Open Scope printing_sugar.
+
+  Definition UnsafeCell_new_def : function := {|
+    f_args := [
+      ("value", (it_layout I32) : layout)
+    ];
+    f_local_vars := [
+      ("__0", (use_layout_alg' (UnsafeCell_st)) : layout);
+      ("__2", (it_layout I32) : layout)
+    ];
+    f_code :=
+      <[
+      "_bb0" :=
+      "__2" <-{ IntOp I32 } use{ IntOp I32 } ("value");
+      "__0" <-{ (use_op_alg' (UnsafeCell_st)) } StructInit UnsafeCell_sls [("value", use{ IntOp I32 } ("__2") : expr)];
+      return (use{ (use_op_alg' (UnsafeCell_st)) } ("__0"))
+      ]>%E $
+      ∅;
+    f_init := "_bb0";
+  |}.
+
+  Definition UnsafeCell_into_inner_def : function := {|
+    f_args := [
+      ("self", (use_layout_alg' (UnsafeCell_st)) : layout)
+    ];
+    f_local_vars := [
+      ("__0", (it_layout I32) : layout)
+    ];
+    f_code :=
+      <[
+      "_bb0" :=
+      "__0" <-{ IntOp I32 } use{ IntOp I32 } (("self") at{ UnsafeCell_sls } "value");
+      return (use{ IntOp I32 } ("__0"))
+      ]>%E $
+      ∅;
+    f_init := "_bb0";
+  |}.
+
+  Definition UnsafeCell_get_old_def : function := {|
+    f_args := [
+      ("self", void* : layout)
+    ];
+    f_local_vars := [
+      ("__0", (it_layout I32) : layout)
+    ];
+    f_code :=
+      <[
+      "_bb0" :=
+      annot: CopyLftNameAnnot "plft3" "ulft__";
+      "__0" <-{ IntOp I32 } use{ IntOp I32 } ((!{ PtrOp } ( "self" )) at{ (UnsafeCell_sls) } "value");
+      return (use{ IntOp I32 } ("__0"))
+      ]>%E $
+      ∅;
+    f_init := "_bb0";
+  |}.
+
+  Definition UnsafeCell_get_def : function := {|
+    f_args := [
+      ("self", void* : layout)
+    ];
+    f_local_vars := [
+      ("__0", void* : layout);
+      ("__2", void* : layout);
+      ("__3", void* : layout)
+    ];
+    f_code :=
+      <[
+      "_bb0" :=
+      annot: CopyLftNameAnnot "plft3" "ulft_1";
+      "__3" <-{ PtrOp } &raw{ Shr } (!{ PtrOp } ( "self" ));
+      "__2" <-{ PtrOp } use{ PtrOp } ("__3");
+      "__0" <-{ PtrOp } use{ PtrOp } ("__2");
+      return (use{ PtrOp } ("__0"))
+      ]>%E $
+      ∅;
+    f_init := "_bb0";
+  |}.
+
+  Definition Cell_new_def (UnsafeCell_new_loc : loc) : function := {|
+    f_args := [
+      ("value", (it_layout I32) : layout)
+    ];
+    f_local_vars := [
+      ("__0", (use_layout_alg' (Cell_st)) : layout);
+      ("__2", (use_layout_alg' (UnsafeCell_st)) : layout);
+      ("__3", (it_layout I32) : layout)
+    ];
+    f_code :=
+      <[
+      "_bb0" :=
+      "__3" <-{ IntOp I32 } use{ IntOp I32 } ("value");
+      "__2" <-{ (use_op_alg' (UnsafeCell_st)) } CallE UnsafeCell_new_loc [] [] [@{expr} use{ IntOp I32 } ("__3")];
+      Goto "_bb1"
+      ]>%E $
+      <[
+      "_bb1" :=
+      "__0" <-{ (use_op_alg' (Cell_st)) } StructInit Cell_sls [("value", use{ (use_op_alg' (UnsafeCell_st)) } ("__2") : expr)];
+      return (use{ (use_op_alg' (Cell_st)) } ("__0"))
+      ]>%E $
+      ∅;
+    f_init := "_bb0";
+  |}.
+
+  Definition Cell_into_inner_def (UnsafeCell_into_inner_loc : loc) : function := {|
+    f_args := [
+      ("self", (use_layout_alg' (Cell_st)) : layout)
+    ];
+    f_local_vars := [
+      ("__0", (it_layout I32) : layout);
+      ("__2", (use_layout_alg' (UnsafeCell_st)) : layout)
+    ];
+    f_code :=
+      <[
+      "_bb0" :=
+      "__2" <-{ (use_op_alg' (UnsafeCell_st)) } use{ (use_op_alg' (UnsafeCell_st)) } (("self") at{ Cell_sls } "value");
+      "__0" <-{ IntOp I32 } CallE UnsafeCell_into_inner_loc [] [] [@{expr} use{ (use_op_alg' (UnsafeCell_st)) } ("__2")];
+      Goto "_bb1"
+      ]>%E $
+      <[
+      "_bb1" :=
+      return (use{ IntOp I32 } ("__0"))
+      ]>%E $
+      ∅;
+    f_init := "_bb0";
+  |}.
+End code.
+
+Section UnsafeCell_ty.
+  Context `{!refinedrustGS Σ}.
+
+  Definition UnsafeCell_ty : type (plist place_rfn [Z : Type]).
+  Proof using  Type*. exact (struct_t UnsafeCell_sls +[(int I32)]). Defined.
+
+  Definition UnsafeCell_rt : Type.
+  Proof using . let __a := eval hnf in (rt_of UnsafeCell_ty) in exact __a. Defined.
+
+  Global Typeclasses Transparent UnsafeCell_ty.
+  Global Typeclasses Transparent UnsafeCell_rt.
+End UnsafeCell_ty.
+Global Arguments UnsafeCell_rt : clear implicits.
+
+Section UnsafeCell_inv_t.
+  Context `{!refinedrustGS Σ}.
+
+  Program Definition UnsafeCell_inv_t_inv_spec : na_ex_inv_def (UnsafeCell_rt) (Z) :=
+    na_mk_ex_inv_def
+      ((Z)%type)
+      (xmap)
+      (λ π inner_rfn 'x, ⌜inner_rfn = -[#(x)]⌝ ∗ ⌜Zeven x⌝ ∗ True)%I
+      [] [].
+
+  Definition UnsafeCell_inv_t : type (Z) :=
+    na_ex_plain_t _ _ UnsafeCell_inv_t_inv_spec UnsafeCell_ty.
+
+  Definition UnsafeCell_inv_t_rt : Type.
+  Proof using. let __a := eval hnf in (rt_of UnsafeCell_inv_t) in exact __a. Defined.
+
+  Global Typeclasses Transparent UnsafeCell_inv_t.
+  Global Typeclasses Transparent UnsafeCell_inv_t_rt.
+End UnsafeCell_inv_t.
+Global Arguments UnsafeCell_inv_t_rt : clear implicits.
+
+Section Cell_ty.
+  Context `{!refinedrustGS Σ}.
+
+  Definition Cell_ty : type (plist place_rfn [UnsafeCell_inv_t_rt : Type]).
+  Proof using  Type*. exact (struct_t Cell_sls +[UnsafeCell_inv_t]). Defined.
+  Definition Cell_rt : Type.
+  Proof using . let __a := eval hnf in (rt_of Cell_ty) in exact __a. Defined.
+
+  Global Typeclasses Transparent Cell_ty.
+  Global Typeclasses Transparent Cell_rt.
+End Cell_ty.
+Global Arguments Cell_rt : clear implicits.
+
+Section Cell_inv_t.
+  Context `{!refinedrustGS Σ}.
+
+  Program Definition Cell_inv_t_inv_spec : na_ex_inv_def (Cell_rt) (Z) :=
+    na_mk_ex_inv_def
+      ((Z)%type)
+      (xmap)
+      (λ π inner_rfn 'x, ⌜inner_rfn = -[#(x)]⌝ ∗ ⌜Zeven x⌝ ∗ True)%I
+      [] [].
+
+  Definition Cell_inv_t : type (Z) :=
+    na_ex_plain_t _ _ Cell_inv_t_inv_spec Cell_ty.
+
+  Definition Cell_inv_t_rt : Type.
+  Proof using . let __a := eval hnf in (rt_of Cell_inv_t) in exact __a. Defined.
+
+  Global Typeclasses Transparent Cell_inv_t.
+  Global Typeclasses Transparent Cell_inv_t_rt.
+End Cell_inv_t.
+Global Arguments Cell_inv_t_rt : clear implicits.
+
+Section specs.
+  Context `{RRGS: !refinedrustGS Σ}.
+
+  Definition type_of_UnsafeCell_new  :=
+    fn(∀ ( *[]) : 0 | ( *[]): ([]) | (x) : (Z), (λ ϝ, []); x :@: (int I32); (λ π : thread_id, (⌜Zeven x⌝)))
+      → ∃ _ : unit, x @ UnsafeCell_inv_t; (λ π : thread_id, True).
+
+  Definition type_of_UnsafeCell_into_inner  :=
+    fn(∀ ( *[]) : 0 | ( *[]): ([]) | (x) : (Z), (λ ϝ, []); x :@: UnsafeCell_inv_t; (λ π : thread_id, True))
+      → ∃ _ : unit, x @ (int I32); (λ π : thread_id, (⌜Zeven x⌝)).
+
+  Definition type_of_UnsafeCell_get_old  :=
+    fn(∀ ( *[ulft_1]) : 1 | ( *[]) : ([]) | (x) : (_), (λ ϝ, []); x :@: (shr_ref ulft_1 UnsafeCell_inv_t); (λ π : thread_id, True))
+      → ∃ _ : unit, x @ (int I32); (λ π : thread_id, (⌜Zeven x⌝)).
+
+  Definition type_of_Cell_new  :=
+    fn(∀ ( *[]) : 0 | ( *[]) : [] | (x) : (Z), (λ ϝ, []); x :@: (int I32); (λ π : thread_id, (⌜Zeven x⌝)))
+      → ∃ _ : unit, x @ Cell_inv_t; (λ π : thread_id, True).
+
+  Definition type_of_Cell_into_inner  :=
+    fn(∀ ( *[]) : 0 | ( *[]) : [] | (x) : (_), (λ ϝ, []); x :@: Cell_inv_t; (λ π : thread_id, True))
+      → ∃ _ : unit, x @ (int I32); (λ π : thread_id, (⌜Zeven x⌝)).
+End specs.
+
+Section proof.
+  Context `{RRGS: !refinedrustGS Σ}.
+
+  Definition UnsafeCell_new_lemma (π : thread_id) : Prop :=
+    syn_type_is_layoutable ((UnsafeCell_sls : syn_type)) →
+    ⊢ typed_function π (UnsafeCell_new_def ) [UnsafeCell_st; IntSynType I32] (<tag_type> type_of_UnsafeCell_new ).
+
+  Definition UnsafeCell_into_inner_lemma (π : thread_id) : Prop :=
+    syn_type_is_layoutable ((UnsafeCell_sls : syn_type)) →
+    ⊢ typed_function π (UnsafeCell_into_inner_def ) [IntSynType I32] (<tag_type> type_of_UnsafeCell_into_inner ).
+
+  Definition UnsafeCell_get_old_lemma (π : thread_id) : Prop :=
+    syn_type_is_layoutable (Cell_st) →
+    ⊢ typed_function π (UnsafeCell_get_old_def ) [IntSynType I32] (<tag_type> type_of_UnsafeCell_get_old ).
+
+  Definition Cell_new_lemma (π : thread_id) : Prop :=
+    ∀ (UnsafeCell_new_loc : loc) ,
+    syn_type_is_layoutable ((UnsafeCell_sls : syn_type)) →
+    syn_type_is_layoutable ((Cell_sls : syn_type)) →
+    UnsafeCell_new_loc ◁ᵥ{π} UnsafeCell_new_loc @ function_ptr [IntSynType I32] (<tag_type> spec! ( *[]) : 0 | ( *[]) : ([]), type_of_UnsafeCell_new (RRGS := RRGS) <MERGE!>) -∗
+    typed_function π (Cell_new_def UnsafeCell_new_loc  ) [Cell_st; UnsafeCell_st; IntSynType I32] (<tag_type> type_of_Cell_new ).
+End proof.
+
+Ltac UnsafeCell_new_prelude :=
+  unfold UnsafeCell_new_lemma;
+  set (FN_NAME := FUNCTION_NAME "UnsafeCell_new");
+  intros;
+  iStartProof;
+  let ϝ := fresh "ϝ" in
+  start_function "UnsafeCell_new" ϝ ( [] ) ( [] ) (  x ) (  x );
+  set (loop_map := BB_INV_MAP (PolyNil));
+  intros arg_value local___0 local___2;
+  init_lfts (named_lft_update "_flft" ϝ $ ∅ );
+  init_tyvars ( ∅ ).
+
+Ltac UnsafeCell_into_inner_prelude :=
+  unfold UnsafeCell_into_inner_lemma;
+  set (FN_NAME := FUNCTION_NAME "UnsafeCell_into_inner");
+  intros;
+  iStartProof;
+  let ϝ := fresh "ϝ" in
+  start_function "UnsafeCell_into_inner" ϝ ( [] ) ( [] ) (  x ) (  x );
+  set (loop_map := BB_INV_MAP (PolyNil));
+  intros arg_self local___0;
+  init_lfts (named_lft_update "_flft" ϝ $ ∅ );
+  init_tyvars ( ∅ ).
+
+Ltac UnsafeCell_get_old_prelude :=
+  unfold UnsafeCell_get_old_lemma;
+  set (FN_NAME := FUNCTION_NAME "Cell_get");
+  intros;
+  iStartProof;
+  let ϝ := fresh "ϝ" in
+  let ulft__ := fresh "ulft__" in
+  start_function "UnsafeCell_get_old" ϝ ( [ ulft__ [] ] ) ( [] ) (  x ) (  x );
+  set (loop_map := BB_INV_MAP (PolyNil));
+  intros arg_self local___0;
+  init_lfts (named_lft_update "ulft__" ulft__ $ named_lft_update "_flft" ϝ $ ∅ );
+  init_tyvars ( ∅ ).
+
+Ltac Cell_new_prelude :=
+  unfold Cell_new_lemma;
+  set (FN_NAME := FUNCTION_NAME "Cell_new");
+  intros;
+  iStartProof;
+  let ϝ := fresh "ϝ" in
+  start_function "Cell_T_new" ϝ ( [] ) ( [] ) (  x ) (  x );
+  set (loop_map := BB_INV_MAP (PolyNil));
+  intros arg_value local___0 local___2 local___3;
+  init_lfts (named_lft_update "_flft" ϝ $ ∅ );
+  init_tyvars ( ∅ ).
+
+Section proof.
+  Context `{!refinedrustGS Σ}.
+
+  Lemma UnsafeCell_new_proof (π : thread_id) :
+    UnsafeCell_new_lemma π.
+  Proof.
+    UnsafeCell_new_prelude.
+
+    repeat liRStep; liShow.
+
+    all: print_remaining_goal.
+    Unshelve. all: sidecond_solver.
+    Unshelve. all: sidecond_hammer.
+    Unshelve. all: print_remaining_sidecond.
+  Qed.
+
+  Lemma UnsafeCell_into_inner_proof (π : thread_id) :
+    UnsafeCell_into_inner_lemma π.
+  Proof.
+    UnsafeCell_into_inner_prelude.
+
+    repeat liRStep; liShow.
+
+    all: print_remaining_goal.
+    Unshelve. all: sidecond_solver.
+    Unshelve. all: sidecond_hammer.
+    Unshelve. all: print_remaining_sidecond.
+  Qed.
+
+  Lemma Cell_new_proof (π : thread_id) :
+    Cell_new_lemma π.
+  Proof.
+    Cell_new_prelude.
+
+    repeat liRStep; liShow.
+
+    all: print_remaining_goal.
+    Unshelve. all: sidecond_solver.
+    Unshelve. all: sidecond_hammer.
+    Unshelve. all: print_remaining_sidecond.
+  Qed.
+
+  Lemma UnsafeCell_get_old_proof (π : thread_id) :
+    UnsafeCell_get_old_lemma π.
+  Proof.
+    UnsafeCell_get_old_prelude.
+
+    do 324 liRStep; liShow.
+
+    (* TODO: This instance isn't properly found *)
+    iApply stratify_ltype_shadowed_shared.
+
+    repeat liRStep; liShow.
+
+    Unshelve. all: sidecond_solver.
+    Unshelve. all: sidecond_hammer.
+    Unshelve. all: print_remaining_sidecond.
+  Qed.
+End proof.