wip bst removeMax, bottom_up_simpl fails because of

(fake-)dependently-typed mk_sized_predicate

LiveVerif/src/LiveVerifExamples/tree_set.v

@@ -217,6 +217,72 @@ Ltac predicates_safe_to_cancel_hook hypPred conclPred ::=
       end
   end.
 
+Ltac provide_new_ghosts_hook ::= manual_new_ghosts.
+
+#[export] Instance spec_of_bst_remove_max: fnspec :=                              .**/
+
+uintptr_t bst_remove_max(uintptr_t c) /**#
+  ghost_args := p s sk (R: mem -> Prop);
+  requires t m := p <> /[0] /\
+                  <{ * allocator
+                     * uintptr p c
+                     * bst' sk s p
+                     * R }> m;
+  ensures t' m' r := t' = t /\ exists sk' q,
+                     s \[r] /\
+                     (forall x, s x -> x <= \[r]) /\
+                     <{ * allocator
+                        * uintptr q c
+                        * bst' sk' (fun x => s x /\ x < \[r]) q
+                        * R }> m' #**/                                     /**.
+Derive bst_remove_max SuchThat (fun_correct! bst_remove_max)
+As bst_remove_max_ok.                                                           .**/
+{                                                                          /**. .**/
+  uintptr_t p = load(c);                                                   /**. .**/
+  uintptr_t res = 0;                                                       /**.
+  (* Local Arguments ready : clear implicits. *)
+  loop invariant above p.
+  delete #(res = ??).
+  move skR before t.
+                                                                                .**/
+  do /* initial_ghosts(s, c, skR, R); decreases skR */ {                   /**. .**/
+    c = p + sizeof(uintptr_t) + 4;                                         /**. .**/
+    p = load(c);                                                           /**. .**/
+    if (p) /* split */ {                                                   /**. .**/
+      /* nothing to do */                                                  /**. .**/
+    }                                                                      /**.
+      instantiate (3 := expr.var "p"). (* <-- need to give loop termination cond
+                                          already here... *)
+      steps.
+      new_ghosts((fun x => (s x /\ v < x)), c, skR, _).
+      steps.
+      { destr (x <=? v). 1: lia. eauto. }
+                                                                                .**/
+    else {                                                                 /**.
+(* bottom_up_simpl_in_hyp fails because it tries to
+   rewrite with (H0 : p = /[0]) in
+
+  H : m |= <{ + uintptr pL
+              + uint 32 v
+              + uintptr p }> p'
+
+  but mk_sized_predicate is too dependently typed for f_equal to work *)
+
+lazymatch goal with
+        | |- wp_cmd _ _ _ _ _ _ =>
+              lazymatch goal with
+              | |- ?G => change (@ready G)
+              end;
+              (* after_command_simpl_hook; <- fails *)
+              unzify;
+              unpurify;
+              set_state displaying
+end.
+
+      (* res = load32(c - 4);     *)                                            .**/
+    }                                                                      /**.
+Abort.
+
 #[export] Instance spec_of_bst_init: fnspec :=                              .**/
 
 void bst_init(uintptr_t p) /**#
@@ -256,6 +322,7 @@ As bst_alloc_node_ok.
   destruct_one_match_hyp; steps.
 Qed.
 
+Ltac provide_new_ghosts_hook ::= guess_new_ghosts.
 
 #[export] Instance spec_of_bst_add: fnspec :=                              .**/
 

bedrock2/src/bedrock2/bottom_up_simpl.v

@@ -2186,6 +2186,24 @@ Section Tests.
       w2 = /[1].
   Proof. intros. bottom_up_simpl_in_goal (). refl. Succeed Qed. Abort.
 
+  Goal forall (hprop: Type),
+       let PS := fun (dummy: hprop) => Z in
+       forall (mk: forall p, PS p -> Prop) (uintptr: Z -> hprop) x y,
+       mk (uintptr x) y ->
+       x = 0 ->
+       True.
+  Proof.
+    intros.
+    Fail bottom_up_simpl_in_hyps ().
+    (* as excepted, but not experienced until now,
+       dependent types break bottom_up_simpl! *)
+    pose proof (f_equal uintptr H0) as A.
+    pose proof (@f_equal hprop (Z -> Prop) mk (uintptr x) (uintptr 0) A).
+    epose proof (@f_equal _ _ _ (uintptr x) (uintptr 0) A).
+    Fail epose proof (@f_equal _ _ mk (uintptr x) (uintptr 0) A).
+    pose proof (@f_equal _ _ (mk: hprop -> Z -> Prop) (uintptr x) (uintptr 0) A).
+  Abort.
+
   Goal forall a b, /[\[a ^+ b]] = a ^+ b.
   Proof. intros. bottom_up_simpl_in_goal (). refl. Succeed Qed. Abort.