From 36668c084aa93ce33f6e343b9a17e69a86043f40 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Lennard=20G=C3=A4her?= <l.gaeher@posteo.de>
Date: Tue, 24 Sep 2024 17:35:46 +0200
Subject: [PATCH] bug fixes in automation

---
 theories/lithium/base.v                   | 13 +++++
 theories/lithium/interpreter.v            |  4 +-
 theories/rust_typing/automation/loc_eq.v  |  2 +-
 theories/rust_typing/automation/simpl.v   |  6 +--
 theories/rust_typing/automation/solvers.v | 38 +++++++++----
 theories/rust_typing/functions.v          |  1 +
 theories/rust_typing/generics.v           |  8 +--
 theories/rust_typing/hlist.v              | 13 -----
 theories/rust_typing/products.v           | 66 ++++++++++++++++++++++-
 theories/rust_typing/programs.v           |  1 +
 theories/rust_typing/shims.v              |  6 ++-
 11 files changed, 120 insertions(+), 38 deletions(-)

diff --git a/theories/lithium/base.v b/theories/lithium/base.v
index 32647658..320fa3e8 100644
--- a/theories/lithium/base.v
+++ b/theories/lithium/base.v
@@ -172,6 +172,19 @@ Lemma list_eq_split {A} i (l1 l2 : list A):
   l1 = l2.
 Proof. move => ??. rewrite -(take_drop i l1) -(take_drop i l2). congruence. Qed.
 
+(** Nested pairs for plist *)
+Section plist.
+  Local Set Universe Polymorphism.
+  Inductive nil_unit: Set := nil_tt: nil_unit.
+  Record cons_prod (A B: Type) : Type := cons_pair { phd' : A; ptl' : B }.
+
+  Context {A} {F : A → Type}.
+  Fixpoint plist (Xl: list A) : Type :=
+    match Xl with [] => nil_unit | X :: Xl' => cons_prod (F X) (plist Xl') end.
+End plist.
+Global Arguments cons_pair {_ _} _ _.
+Global Arguments phd' {_ _} _.
+Global Arguments ptl' {_ _} _.
 
 (** * typeclasses *)
 Inductive TCOneIsSome {A} : option A → option A → Prop :=
diff --git a/theories/lithium/interpreter.v b/theories/lithium/interpreter.v
index 8c9b2ca5..5dbde3bb 100644
--- a/theories/lithium/interpreter.v
+++ b/theories/lithium/interpreter.v
@@ -219,10 +219,12 @@ Ltac liExist protect :=
         | prod _ _ => apply: tac_exist_prod
         | sigT _ => apply: tac_exist_sigT
         | unit => exists tt
+        | nil_unit => exists nil_tt
+        | @plist _ _ [] => exists nil_tt
         | _ =>
             first [
                 let p := constr:(_ : SimplExist A P _) in
-                refine (@simpl_exist_proof _ _ _ p _)
+                refine (@simpl_exist_proof A P _ p _)
               |
                 lazymatch protect with
                 | true => let Hevar := create_protected_evar A in exists (protected Hevar)
diff --git a/theories/rust_typing/automation/loc_eq.v b/theories/rust_typing/automation/loc_eq.v
index 8238031e..ee2af2c4 100644
--- a/theories/rust_typing/automation/loc_eq.v
+++ b/theories/rust_typing/automation/loc_eq.v
@@ -107,7 +107,7 @@ Section test.
   solve_loc_eq. Qed.
 
   Goal (l offsetst{IntSynType u8}â‚— n1) = l +â‚— (ly_size u8 * n1).
-  init_cache; solve_loc_eq. Qed.
+  init_cache. solve_loc_eq. Qed.
 
   Goal (l offsetst{IntSynType usize_t}â‚— n1) = l +â‚— (ly_size usize_t * n1).
   init_cache; solve_loc_eq. Qed.
diff --git a/theories/rust_typing/automation/simpl.v b/theories/rust_typing/automation/simpl.v
index 2fadb160..3e62431a 100644
--- a/theories/rust_typing/automation/simpl.v
+++ b/theories/rust_typing/automation/simpl.v
@@ -80,11 +80,7 @@ Global Instance simpl_exist_hlist_cons {X} (F : X → Type) (x : X) xs (Q : hlis
 Proof.
   intros (p & ps & Hx). exists (p +:: ps). done.
 Qed.
-Global Instance simpl_exist_plist_nil {X} (F : X → Type) Q :
-  SimplExist (plist F []) Q (Q -[]).
-Proof.
-  rewrite /SimplExist. naive_solver.
-Qed.
+(* The instance for plist _ [] is built into Lithium's liExist *)
 Global Instance simpl_exist_plist_cons {X} (F : X → Type) (x : X) xs (Q : plist F (x :: xs) → Prop) :
   SimplExist (plist F (x :: xs)) Q (∃ p : F x, ∃ ps : plist F xs, Q (p -:: ps)).
 Proof.
diff --git a/theories/rust_typing/automation/solvers.v b/theories/rust_typing/automation/solvers.v
index 7f38947d..56562163 100644
--- a/theories/rust_typing/automation/solvers.v
+++ b/theories/rust_typing/automation/solvers.v
@@ -1742,21 +1742,39 @@ Ltac maybe_simplify_layout ly :=
   | use_union_layout_alg' _ => simplify_layout_go ly
   | ot_layout _ => simplify_layout_go ly
   end.
-Ltac simplify_layout_goal :=
-  repeat match goal with
-  | |- context[?ly] =>
-      match type of ly with
-      | layout => maybe_simplify_layout ly
-      end
-  end.
-Ltac simplify_layout_assum :=
-  repeat match goal with
+Ltac simplify_layout_assum_step :=
+  match goal with
   | H: context[?ly] |- _ =>
       assert_is_not_cached H;
       match type of ly with
       | layout => maybe_simplify_layout ly
       end
   end.
+Ltac simplify_layout_assum :=
+  repeat simplify_layout_assum_step.
+Ltac simplify_layout_in A :=
+  match A with
+  | context[use_layout_alg' ?st] => simplify_layout_go (use_layout_alg' st)
+  | context[use_struct_layout_alg' ?st] => simplify_layout_go (use_struct_layout_alg' st)
+  | context[use_enum_layout_alg' ?st] => simplify_layout_go (use_enum_layout_alg' st)
+  | context[use_union_layout_alg' ?st] => simplify_layout_go (use_union_layout_alg' st)
+  | context[ot_layout ?ot] => simplify_layout_go (ot_layout ot)
+  end.
+Ltac simplify_layout_goal_step :=
+  match goal with
+  (* If we are working on a Lithium goal, don't simplify in the continuation *)
+  | |- envs_entails _ (?A _) =>
+      simplify_layout_in A
+  | |- envs_entails ?H _ =>
+      simplify_layout_in H
+  | |- ?H ∧ envs_entails _ _ =>
+      simplify_layout_in H
+  | |- ?H → envs_entails _ _ =>
+      simplify_layout_in H
+  | |- ?G => simplify_layout_in G
+  end.
+Ltac simplify_layout_goal :=
+  repeat simplify_layout_goal_step.
 
 (** Solve goals of the form [layout_wf ly]. *)
 Section layout.
@@ -1882,7 +1900,7 @@ Ltac solve_layout_alg_prepare :=
   lazymatch goal with
   | |- syn_type_is_layoutable ?st => refine (syn_type_is_layoutable_layout_tac st _ _)
   | |- use_layout_alg ?st = Some ?ly => refine (use_layout_alg_layout_tac st ly _)
-  | |- use_layout_alg' ?st = ?ly => refine (use_layout_alg'_layout_tac st ly)
+  | |- use_layout_alg' ?st = ?ly => refine (use_layout_alg'_layout_tac st ly _)
   | |- syn_type_has_layout ?st ?ly => idtac
   (* structs *)
   | |- use_struct_layout_alg ?sls = ?Some ?sl => refine (use_struct_layout_alg_layout_tac _ _ _)
diff --git a/theories/rust_typing/functions.v b/theories/rust_typing/functions.v
index ec835f88..974179d7 100644
--- a/theories/rust_typing/functions.v
+++ b/theories/rust_typing/functions.v
@@ -534,6 +534,7 @@ Ltac get_params_of_fntype x :=
   | prod_vec _ _ → plist _ _ → ?A → fn_params =>
       let B := eval simpl in A in
       constr:(B)
+  | _ → ?A => get_params_of_fntype A
   end.
 Notation "<get_params_of> x" := (
   ltac:(
diff --git a/theories/rust_typing/generics.v b/theories/rust_typing/generics.v
index 24d0088e..11b530d2 100644
--- a/theories/rust_typing/generics.v
+++ b/theories/rust_typing/generics.v
@@ -125,11 +125,11 @@ Definition spec_with `{!typeGS Σ} (lfts : nat) (rts : list Type) (SPEC : Type)
   prod_vec lft lfts → plist type rts → SPEC.
 Arguments spec_with {_ _} / _ _ .
 
-Notation "x '<TY>' T" := (spec_instantiate_typaram_fst _ _ T x) (left associativity, at level 81) : stdpp_scope.
-Notation "x '<TY>@{' n '}' T" := (spec_instantiate_typaram _ n _ T x) (left associativity, at level 81) : stdpp_scope.
-Notation "x '<LFT>' T" := (spec_instantiate_lft_fst _ T x) (left associativity, at level 81) : stdpp_scope.
+Notation "x '<TY>' T" := (spec_instantiate_typaram_fst _ _ T x) (left associativity, at level 81, only printing) : stdpp_scope.
+Notation "x '<TY>@{' n '}' T" := (spec_instantiate_typaram _ n _ T x) (left associativity, at level 81, only printing) : stdpp_scope.
+Notation "x '<LFT>' T" := (spec_instantiate_lft_fst _ T x) (left associativity, at level 81, only printing) : stdpp_scope.
 Notation "x '<INST!>'" := (spec_instantiated x) (left associativity, at level 81) : stdpp_scope.
-Notation "x '<MERGE!>'" := (spec_collapse_params _ _ x) (left associativity, at level 181) : stdpp_scope.
+Notation "x '<MERGE!>'" := (spec_collapse_params _ _ x) (left associativity, at level 181, only printing) : stdpp_scope.
 
 
 Notation "x '<TY>' T" := (
diff --git a/theories/rust_typing/hlist.v b/theories/rust_typing/hlist.v
index 32961391..a98cb192 100644
--- a/theories/rust_typing/hlist.v
+++ b/theories/rust_typing/hlist.v
@@ -190,19 +190,6 @@ Notation "( fl +$.)" := (happly fl) (only parsing).
 
 (** * Passive Heterogeneous List *)
 (** Defined as nested pairs *)
-Inductive nil_unit: Set := nil_tt: nil_unit.
-Record cons_prod (A B: Type) : Type := cons_pair { phd' : A; ptl' : B }.
-Arguments cons_pair {_ _} _ _.
-Arguments phd' {_ _} _.
-Arguments ptl' {_ _} _.
-
-Section plist.
-  Context {A} {F : A → Type}.
-  #[universes(polymorphic)]
-  Fixpoint plist (Xl: list A) : Type :=
-    match Xl with [] => nil_unit | X :: Xl' => cons_prod (F X) (plist Xl') end.
-End plist.
-
 Definition pcons {A} {F : A → Type} {a X} (hd : F a) (tl : plist X) : plist (a :: X) :=
   cons_pair hd tl.
 Definition pnil {A} {F : A → Type} : plist (F := F) [] := nil_tt.
diff --git a/theories/rust_typing/products.v b/theories/rust_typing/products.v
index d85d0c78..32a86d7a 100644
--- a/theories/rust_typing/products.v
+++ b/theories/rust_typing/products.v
@@ -3787,8 +3787,70 @@ Section rules.
 
   (* TODO prove_place_cond *)
 
-  (* TODO resolve hgost *)
-
+  (** resolve_ghost instances *)
+  Lemma resolve_ghost_struct_Owned {rts} π E L l (lts : hlist ltype rts) sls γ wl rm lb T :
+    find_observation ((plist place_rfn rts)) γ FindObsModeDirect (λ or,
+        match or with
+        | None => ⌜rm = ResolveTry⌝ ∗ T L (PlaceGhost γ) True false
+        | Some r => T L (PlaceIn $ r) True true
+        end)
+    ⊢ resolve_ghost π E L rm lb l (StructLtype lts sls) (Owned wl) (PlaceGhost γ) T.
+  Proof.
+    iIntros "Ha" (???) "#CTX #HE HL Hl".
+    iMod ("Ha" with "[//]") as "[(%r' & HObs & Ha) | (_ & Ha)]".
+    - rewrite ltype_own_struct_unfold /struct_ltype_own.
+      iDestruct "Hl" as "(%sl & ? & ? & ? & ? & ? & %rs & Hinterp & ?)".
+      simpl. iPoseProof (gvar_pobs_agree_2 with "Hinterp HObs") as "#<-".
+      iExists _, _, _, _. iFrame. iApply maybe_logical_step_intro.
+      iL. rewrite ltype_own_struct_unfold /struct_ltype_own.
+      iExists _. iFrame. iExists _. iR. by iFrame.
+    - iExists _, _, _, _. iFrame.  iApply maybe_logical_step_intro. by iFrame.
+  Qed.
+  Definition resolve_ghost_struct_Owned_inst := [instance @resolve_ghost_struct_Owned].
+  Global Existing Instance resolve_ghost_struct_Owned_inst.
+
+  Lemma resolve_ghost_struct_Uniq {rts} π E L l (lts : hlist ltype rts) sls γ rm lb κ γ' T :
+    find_observation ((plist place_rfn rts)) γ FindObsModeDirect (λ or,
+        match or with
+        | None => ⌜rm = ResolveTry⌝ ∗ T L (PlaceGhost γ) True false
+        | Some r => T L (PlaceIn $ r) True true
+        end)
+    ⊢ resolve_ghost π E L rm lb l (StructLtype lts sls) (Uniq κ γ') (PlaceGhost γ) T.
+  Proof.
+    iIntros "Ha" (???) "#CTX #HE HL Hl".
+    iMod ("Ha" with "[//]") as "[(%r' & HObs & Ha) | (_ & Ha)]".
+    - rewrite ltype_own_struct_unfold /struct_ltype_own.
+      iDestruct "Hl" as "(%ly & ? & ? & ? & ? & ? & Hinterp & ?)".
+      simpl.
+      iPoseProof (Rel2_use_pobs with "HObs Hinterp") as "(%r2 & Hobs & ->)".
+      iExists _, _, _, _. iFrame. iApply maybe_logical_step_intro.
+      iL. rewrite ltype_own_struct_unfold /struct_ltype_own.
+      iExists _. iFrame. done.
+    - iExists _, _, _, _. iFrame.  iApply maybe_logical_step_intro. by iFrame.
+  Qed.
+  Definition resolve_ghost_struct_Uniq_inst := [instance @resolve_ghost_struct_Uniq].
+  Global Existing Instance resolve_ghost_struct_Uniq_inst.
+
+  Lemma resolve_ghost_struct_Shared {rts} π E L l (lts : hlist ltype rts) sls γ rm lb κ T :
+    find_observation (plist place_rfn rts) γ FindObsModeDirect (λ or,
+        match or with
+        | None => ⌜rm = ResolveTry⌝ ∗ T L (PlaceGhost γ) True false
+        | Some r => T L (#r) True true
+        end)
+    ⊢ resolve_ghost π E L rm lb l (StructLtype lts sls) (Shared κ) (PlaceGhost γ) T.
+  Proof.
+    iIntros "Ha" (???) "#CTX #HE HL Hl".
+    iMod ("Ha" with "[//]") as "[(%r' & HObs & Ha) | (_ & Ha)]".
+    - rewrite ltype_own_struct_unfold /struct_ltype_own.
+      iDestruct "Hl" as "(%sl & ? & ? & ? & ? & %rs & Hinterp & ?)".
+      simpl. iPoseProof (gvar_pobs_agree_2 with "Hinterp HObs") as "#<-".
+      iExists _, _, _, _. iFrame. iApply maybe_logical_step_intro.
+      iL. rewrite ltype_own_struct_unfold /struct_ltype_own.
+      iExists _. iFrame. iExists _. iR. by iFrame.
+    - iExists _, _, _, _. iFrame. iApply maybe_logical_step_intro. by iFrame.
+  Qed.
+  Definition resolve_ghost_struct_Shared_inst := [instance @resolve_ghost_struct_Shared].
+  Global Existing Instance resolve_ghost_struct_Shared_inst.
 End rules.
 
 Global Typeclasses Opaque MutEqltypeStructHFR.
diff --git a/theories/rust_typing/programs.v b/theories/rust_typing/programs.v
index 24c12f54..1f2784a4 100644
--- a/theories/rust_typing/programs.v
+++ b/theories/rust_typing/programs.v
@@ -4014,6 +4014,7 @@ Ltac generate_i2p_instance_to_tc_hook arg c ::=
   | typed_annot_stmt ?a => constr:(TypedAnnotStmt a)
   | introduce_with_hooks ?E ?L ?P => constr:(IntroduceWithHooks E L P)
   | subsume_full ?E ?L ?wl ?P1 ?P2 => constr:(SubsumeFull E L wl P1 P2)
+  | resolve_ghost ?π ?E ?L ?rm ?f ?l ?lt ?k ?r => constr:(ResolveGhost π E L rm f l lt k r)
   | prove_with_subtype ?E ?L ?wl ?pm ?P => constr:(ProveWithSubtype E L wl pm P)
   | typed_on_endlft ?π ?E ?L ?κ ?worklist => constr:(TypedOnEndlft π E L κ worklist)
   | weak_subtype ?E ?L ?r1 ?r2 ?ty1 ?ty2 => constr:(Subtype E L r1 r2 ty1 ty2)
diff --git a/theories/rust_typing/shims.v b/theories/rust_typing/shims.v
index 863837c8..f2b47941 100644
--- a/theories/rust_typing/shims.v
+++ b/theories/rust_typing/shims.v
@@ -130,8 +130,10 @@ Lemma mem_align_of_typed `{RRGS : !refinedrustGS Σ} π T_rt T_st T_ly :
   ⊢ typed_function π (mem_align_of T_st) [] (<tag_type> type_of_mem_align_of T_rt T_st).
 Proof.
   start_function "mem_align_of" ( () ) ( [T_ty []] ) ( () ).
-  repeat liRStep. Unshelve.
+  repeat liRStep; liShow.
+  Unshelve.
   all: unshelve_sidecond.
+  simplify_layout_goal.
   by apply ly_align_in_usize.
 Qed.
 
@@ -279,7 +281,7 @@ Proof.
   iApply (typed_goto_acc _ _ _ _ _ loop_inv).
   { unfold_code_marker_and_compute_map_lookup. }
   liRStep; liShow. iExists 0%nat.
-  repeat liRStep. liShow.
+  repeat liRStep; liShow.
   iRename select (loop_inv _ _) into "Hinv".
   iDestruct "Hinv" as "(%i & -> & -> & Hcredit & Hlen & Hcount & Hsrc & Hdst & Hs & Ht)".
   repeat liRStep; liShow.
-- 
GitLab