let vrefine (v: vprop) (p: (normal (t_of v) -> Tot prop)) = VUnit (vrefine' v p)
let vrefine (v: vprop) (p: (normal (t_of v) -> Tot prop)) =
VUnit (vrefine' v p)
Steel.Effect.Common.fsti.checked
Steel.Memory.fsti.checked prims.fst.checked FStar.Tactics.V2.fst.checked FStar.Tactics.CanonCommMonoidSimple.Equiv.fst.checked FStar.String.fsti.checked FStar.Squash.fsti.checked FStar.Set.fsti.checked FStar.Reflection.V2.Derived.Lemmas.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.Base.fst.checked FStar.List.Tot.fst.checked FStar.Ghost.fsti.checked FStar.FunctionalExtensionality.fsti.checked FStar.Classical.fsti.checked FStar.Algebra.CommMonoid.Equiv.fst.checked
Steel.Effect.Common.fsti
Steel.Effect.Common.vprop Steel.Effect.Common.normal Steel.Effect.Common.t_of Prims.prop Steel.Effect.Common.VUnit Steel.Effect.Common.vrefine'
(*
   Copyright 2020 Microsoft Research

   Licensed under the Apache License, Version 2.0 (the "License");
   you may not use this file except in compliance with the License.
   You may obtain a copy of the License at

       http://www.apache.org/licenses/LICENSE-2.0

   Unless required by applicable law or agreed to in writing, software
   distributed under the License is distributed on an "AS IS" BASIS,
   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
   See the License for the specific language governing permissions and
   limitations under the License.
*)

module Steel.Effect.Common
open Steel.Memory
module Mem = Steel.Memory
module FExt = FStar.FunctionalExtensionality
open FStar.Ghost

/// This module provides various predicates and functions which are common to the
/// different Steel effects.
/// It also contains the tactic responsible for frame inference through a variant of AC-unification

#set-options "--ide_id_info_off"

(* Normalization helpers *)

irreducible let framing_implicit : unit = ()
irreducible let __steel_reduce__ : unit = ()
/// An internal attribute for finer-grained normalization in framing equalities
irreducible let __inner_steel_reduce__ : unit = ()
irreducible let __reduce__ : unit = ()
irreducible let smt_fallback : unit = ()
irreducible let ite_attr : unit = ()

// Needed to avoid some logical vs prop issues during unification with no subtyping
[@@__steel_reduce__]
unfold
let true_p : prop = True

module T = FStar.Tactics.V2

let join_preserves_interp (hp:slprop) (m0:hmem hp) (m1:mem{disjoint m0 m1})
: Lemma
  (interp hp (join m0 m1))
  [SMTPat (interp hp (join m0 m1))]
= let open Steel.Memory in
  intro_emp m1;
  intro_star hp emp m0 m1;
  affine_star hp emp (join m0 m1)

(* Definition of a selector for a given slprop *)

/// A selector of type `a` for a separation logic predicate hp is a function
/// from a memory where the predicate hp holds, which returns a value of type `a`.
/// The effect GTot indicates that selectors are ghost functions, used for specification
/// and proof purposes only
let selector' (a:Type0) (hp:slprop) = hmem hp -> GTot a

/// Self-framing property for selectors
let sel_depends_only_on (#a:Type) (#hp:slprop) (sel:selector' a hp) =
  forall (m0:hmem hp) (m1:mem{disjoint m0 m1}).
    (interp_depends_only_on hp; (
    sel m0 == sel (join m0 m1)))

/// Additional property that selectors must satisfy, related to internals of
/// the Steel memory model encoding
let sel_depends_only_on_core (#a:Type) (#hp:slprop) (sel:selector' a hp) =
  forall (m0:hmem hp). sel m0 == sel (core_mem m0)

/// Full definition of a selector, as a function which satisfies the two predicates above
let selector (a:Type) (hp:slprop) : Type =
  sel:selector' a hp{sel_depends_only_on sel /\ sel_depends_only_on_core sel}

/// The basis of our selector framework: Separation logic assertions enhanced with selectors
/// Note that selectors are "optional", it is always possible to use a non-informative selector,
/// such as fun _ -> () and to rely on the standard separation logic reasoning
[@@ erasable]
noeq
type vprop' =
  { hp: slprop u#1;
    t:Type0;
    sel: selector t hp}

(* Lifting the star operator to an inductive type makes normalization
   and implementing some later functions easier *)
[@@__steel_reduce__; erasable]
noeq
type vprop =
  | VUnit : vprop' -> vprop
  | VStar: vprop -> vprop -> vprop

(* A generic lift from slprop to vprop with a non-informative selector *)

[@@ __steel_reduce__]
let to_vprop' (p:slprop) = {hp = p; t = unit; sel = fun _ -> ()}

[@@ __steel_reduce__]
unfold
let to_vprop (p:slprop) = VUnit (to_vprop' p)

/// Normalization steps for norm below.
/// All functions marked as `unfold`, or with the `__steel_reduce__` attribute will be reduced,
/// as well as some functions internal to the selector framework
unfold
let normal_steps =
   [delta_attr [`%__steel_reduce__; `%__inner_steel_reduce__];
    delta_only [`%Mkvprop'?.t; `%Mkvprop'?.hp; `%Mkvprop'?.sel;
      `%FStar.Algebra.CommMonoid.Equiv.__proj__CM__item__mult;
      `%FStar.Algebra.CommMonoid.Equiv.__proj__CM__item__unit];
    delta_qualifier ["unfold"];
    iota;zeta;primops; simplify]

/// The core normalization primitive used to simplify Verification Conditions before encoding
/// them to an SMT solver.
unfold
let normal (#a:Type) (x:a) = norm normal_steps x

/// An abbreviation for the VStar constructor, allowing to use it with infix notation
[@@ __steel_reduce__; __reduce__]
let star = VStar

/// Extracting the underlying separation logic assertion from a vprop
[@@ __steel_reduce__]
let rec hp_of (p:vprop) = match p with
  | VUnit p -> p.hp
  | VStar p1 p2 -> hp_of p1 `Mem.star` hp_of p2

/// Extracting the selector type from a vprop
[@@ __steel_reduce__]
let rec t_of (p:vprop) = match p with
  | VUnit p -> p.t
  | VStar p1 p2 -> t_of p1 * t_of p2

/// Extracting the selector from a vprop
[@@ __steel_reduce__]
let rec sel_of (p:vprop) : GTot (selector (t_of p) (hp_of p)) = match p with
  | VUnit p -> fun h -> p.sel h
  | VStar p1 p2 ->
     let sel1 = sel_of p1 in
     let sel2 = sel_of p2 in
     fun h -> (sel1 h, sel2 h)

/// Type abbreviations for separation logic pre- and postconditions of the Steel effects
type pre_t = vprop
type post_t (a:Type) = a -> vprop

/// An annotation to indicate which separation logic predicates correspond to monadic computations
/// These computations are handled in a specific manner in the framing tactic; they correspond to places where
/// the context shrinks from all local variables in the computation to variables available at the toplevel
let return_pre (p:vprop) : vprop = p

noextract
let hmem (p:vprop) = hmem (hp_of p)

/// Abstract predicate for vprop implication. Currently implemented as an implication on the underlying slprop
val can_be_split (p q:pre_t) : Type0

/// Exposing the implementation of `can_be_split` when needed for proof purposes
val reveal_can_be_split (_:unit) : Lemma
  (forall p q. can_be_split p q == Mem.slimp (hp_of p) (hp_of q))

/// A targeted version of the above
val can_be_split_interp (r r':vprop) (h:hmem r)
  : Lemma (requires can_be_split r r')
          (ensures interp (hp_of r') h)


/// A dependent version of can_be_split, to be applied to dependent postconditions
let can_be_split_forall (#a:Type) (p q:post_t a) = forall x. can_be_split (p x) (q x)

/// A version of can_be_split which is indexed by a proposition, which can be used for equalities abduction
let can_be_split_dep (p:prop) (t1 t2:pre_t) = p ==> can_be_split t1 t2

/// A dependent version of the above predicate
let can_be_split_forall_dep (#a:Type) (p:a -> prop) (t1 t2:post_t a) =
  forall (x:a). p x ==> can_be_split (t1 x) (t2 x)

(* Some lemmas about the can_be_split* predicates,
  to be used as rewriting rules for the abstract predicates *)

val can_be_split_trans (p q r:vprop)
: Lemma
  (requires p `can_be_split` q /\ q `can_be_split` r)
  (ensures p `can_be_split` r)

let can_be_split_trans_rev (p q r:vprop)
: Lemma
  (requires q `can_be_split` r /\ p `can_be_split` q)
  (ensures p `can_be_split` r)
= can_be_split_trans p q r

val can_be_split_star_l (p q:vprop)
: Lemma
  (ensures (p `star` q) `can_be_split` p)
  [SMTPat ((p `star` q) `can_be_split` p)]

val can_be_split_star_r (p q:vprop)
: Lemma
  (ensures (p `star` q) `can_be_split` q)
  [SMTPat ((p `star` q) `can_be_split` q)]

val can_be_split_refl (p:vprop)
: Lemma (p `can_be_split` p)
[SMTPat (p `can_be_split` p)]


val can_be_split_congr_l
  (p q r: vprop)
: Lemma
  (requires (p `can_be_split` q))
  (ensures ((p `star` r) `can_be_split` (q `star` r)))

val can_be_split_congr_r
  (p q r: vprop)
: Lemma
  (requires (p `can_be_split` q))
  (ensures ((r `star` p) `can_be_split` (r `star` q)))

let prop_and (p1 p2: prop) : Tot prop = p1 /\ p2

let can_be_split_forall_dep_trans_rev
  (#a: Type)
  (cond1 cond2: a -> prop)
  (p q r: post_t a)
: Lemma
  (requires (can_be_split_forall_dep cond2 q r /\ can_be_split_forall_dep cond1 p q))
  (ensures (can_be_split_forall_dep (fun x -> cond1 x `prop_and` cond2 x) p r))
=
  Classical.forall_intro_3 (fun x y z -> Classical.move_requires (can_be_split_trans x y) z)

let can_be_split_forall_dep_congr_l
  (#a: Type)
  (cond: a -> prop)
  (p q r: post_t a)
: Lemma
  (requires (can_be_split_forall_dep cond p q))
  (ensures (can_be_split_forall_dep cond (fun x -> p x `star` r x) (fun x -> q x `star` r x)))
=
  Classical.forall_intro_3 (fun x y z -> Classical.move_requires (can_be_split_congr_l x y) z)

let can_be_split_forall_dep_congr_r
  (#a: Type)
  (cond: a -> prop)
  (p q r: post_t a)
: Lemma
  (requires (can_be_split_forall_dep cond p q))
  (ensures (can_be_split_forall_dep cond (fun x -> r x `star` p x) (fun x -> r x `star` q x)))
=
  Classical.forall_intro_3 (fun x y z -> Classical.move_requires (can_be_split_congr_r x y) z)

/// To simplify the implementation of the framing tactic, dependent equivalence
/// is defined as a double dependent implication
let equiv_forall (#a:Type) (t1 t2:post_t a) : Type0
  = t1 `can_be_split_forall` t2 /\ t2 `can_be_split_forall` t1

/// This equivalence models a context restriction at the end of a Steel computation;
/// note that t2 does not depend on the value of type `a`, but the two vprops must be
///  equivalent
let can_be_split_post (#a #b:Type) (t1:a -> post_t b) (t2:post_t b) =
  forall (x:a). equiv_forall (t1 x) t2

/// Lifting the equivalence relation to vprops. Two vprops are equivalent if the underlying slprops
/// are equivalent
val equiv (p q:vprop) : prop
/// Revealing the definition of vprop equivalence when needed for proof purposes.
/// In other cases, the predicate is abstract
val reveal_equiv (p q:vprop) : Lemma (p `equiv` q <==> hp_of p `Mem.equiv` hp_of q)

(* A restricted view of the heap,
   that only allows to access selectors of the current slprop *)

let rmem' (pre:vprop) =
  FExt.restricted_g_t
  (r0:vprop{can_be_split pre r0})
  (fun r0 -> normal (t_of r0))

/// Ensuring that rmems encapsulate the structure induced by the separation logic star
val valid_rmem (#frame:vprop) (h:rmem' frame) : prop

unfold
let rmem (pre:vprop) = h:rmem' pre{valid_rmem h}

/// Exposing the definition of mk_rmem to better normalize Steel VCs
unfold noextract
let unrestricted_mk_rmem (r:vprop) (h:hmem r) = fun (r0:vprop{r `can_be_split` r0}) ->
  can_be_split_interp r r0 h;
  sel_of r0 h

[@@ __inner_steel_reduce__]
noextract
let mk_rmem' (r:vprop) (h:hmem r) : Tot (rmem' r) =
   FExt.on_dom_g
     (r0:vprop{r `can_be_split` r0})
     (unrestricted_mk_rmem r h)

val lemma_valid_mk_rmem (r:vprop) (h:hmem r) : Lemma (valid_rmem (mk_rmem' r h))

[@@ __inner_steel_reduce__]
noextract
let mk_rmem (r:vprop) (h:hmem r) : Tot (rmem r) =
  lemma_valid_mk_rmem r h;
  mk_rmem' r h

val reveal_mk_rmem (r:vprop) (h:hmem r) (r0:vprop{r `can_be_split` r0})
  : Lemma (ensures reveal_can_be_split(); (mk_rmem r h) r0 == sel_of r0 h)

(* Logical pre and postconditions can only access the restricted view of the heap *)

type req_t (pre:pre_t) = rmem pre -> Type0
type ens_t (pre:pre_t) (a:Type) (post:post_t a) =
  rmem pre -> (x:a) -> rmem (post x) -> Type0

(* Empty assertion *)
val emp : vprop

/// When needed for proof purposes, the empty assertion is a direct lift of the
/// empty assertion from Steel.Memory
val reveal_emp (_:unit) : Lemma (hp_of emp == Mem.emp /\ t_of emp == unit)

/// Lifting pure predicates to vprop
[@@__steel_reduce__]
unfold let pure (p:prop) = to_vprop (pure p)

/// Framing predicates for the Steel effect. If the current computation has already
/// been framed, then the additional frame is the empty predicate
let maybe_emp (framed:bool) (frame:pre_t) = if framed then frame == emp else True
/// Dependent version of the above predicate, usable in dependent postconditions
let maybe_emp_dep (#a:Type) (framed:bool) (frame:post_t a) =
  if framed then (forall x. frame x == emp) else True

(* focus_rmem is an additional restriction of our view of memory.
   We expose it here to be able to reduce through normalization;
   Any valid application of focus_rmem h will be reduced to the application of h *)

[@@ __steel_reduce__]
unfold
let unrestricted_focus_rmem (#r:vprop) (h:rmem r) (r0:vprop{r `can_be_split` r0})
  = fun (r':vprop{can_be_split r0 r'}) -> can_be_split_trans r r0 r'; h r'

[@@ __inner_steel_reduce__]
let focus_rmem' (#r: vprop) (h: rmem r) (r0: vprop{r `can_be_split` r0}) : Tot (rmem' r0)
 = FExt.on_dom_g
   (r':vprop{can_be_split r0 r'})
   (unrestricted_focus_rmem h r0)

val lemma_valid_focus_rmem (#r:vprop) (h:rmem r) (r0:vprop{r `can_be_split` r0})
  : Lemma (valid_rmem (focus_rmem' h r0))

[@@ __inner_steel_reduce__]
let focus_rmem (#r:vprop) (h:rmem r) (r0:vprop{r `can_be_split` r0}) : Tot (rmem r0) =
  lemma_valid_focus_rmem h r0;
  focus_rmem' h r0

/// Exposing that calling focus_rmem on the current context corresponds to an equality
let focus_rmem_refl (r:vprop) (h:rmem r)
  : Lemma (focus_rmem #r h r == h)
  = FStar.FunctionalExtensionality.extensionality_g _ _ (focus_rmem #r h r) h

open FStar.Tactics.V2

/// State that all "atomic" subresources have the same selectors on both views.
/// The predicate has the __steel_reduce__ attribute, ensuring that VC normalization
/// will reduce it to a conjunction of equalities on atomic subresources
/// This predicate is also marked as `strict_on_arguments` on [frame], ensuring that
/// it will not be reduced when the frame is symbolic
/// Instead, the predicate will be rewritten to an equality using `lemma_frame_equalities` below
[@@ __steel_reduce__; strict_on_arguments [0]]
let rec frame_equalities'
  (frame:vprop)
  (h0:rmem frame) (h1:rmem frame) : Type0
  = begin match frame with
    | VUnit p -> h0 frame == h1 frame
    | VStar p1 p2 ->
        can_be_split_star_l p1 p2;
        can_be_split_star_r p1 p2;

        let h01 = focus_rmem h0 p1 in
        let h11 = focus_rmem h1 p1 in

        let h02 = focus_rmem h0 p2 in
        let h12 = focus_rmem h1 p2 in


        frame_equalities' p1 h01 h11 /\
        frame_equalities' p2 h02 h12
    end

/// This lemma states that frame_equalities is the same as an equality on the top-level frame.
/// The uncommon formulation with an extra [p] is needed to use in `rewrite_with_tactic`,
/// where the goal is of the shape `frame_equalities frame h0 h1 == ?u`
/// The rewriting happens below, in `frame_vc_norm`
val lemma_frame_equalities (frame:vprop) (h0:rmem frame) (h1:rmem frame) (p:Type0)
  : Lemma
    (requires (h0 frame == h1 frame) == p)
    (ensures frame_equalities' frame h0 h1 == p)

/// A special case for frames about emp.
val lemma_frame_emp (h0:rmem emp) (h1:rmem emp) (p:Type0)
  : Lemma (requires True == p)
          (ensures frame_equalities' emp h0 h1 == p)

/// A variant of conjunction elimination, suitable to the equality goals during rewriting
val elim_conjunction (p1 p1' p2 p2':Type0)
  : Lemma (requires p1 == p1' /\ p2 == p2')
          (ensures (p1 /\ p2) == (p1' /\ p2'))

/// Normalization and rewriting step for generating frame equalities.
/// The frame_equalities function has the strict_on_arguments attribute on the [frame],
/// ensuring that it is not reduced when the frame is symbolic.
/// When that happens, we want to replace frame_equalities by an equality on the frame,
/// mimicking reduction
[@@plugin]
let frame_vc_norm () : Tac unit = with_compat_pre_core 0 (fun _ ->
  // Do not normalize mk_rmem/focus_rmem to simplify application of
  // the reflexivity lemma on frame_equalities'
  norm [delta_attr [`%__steel_reduce__];
    delta_only [`%Mkvprop'?.t; `%Mkvprop'?.hp; `%Mkvprop'?.sel;
      `%FStar.Algebra.CommMonoid.Equiv.__proj__CM__item__mult;
      `%FStar.Algebra.CommMonoid.Equiv.__proj__CM__item__unit];
    delta_qualifier ["unfold"];
    iota;zeta;primops; simplify];

  // After reduction, the term to rewrite might be of the shape
  // (frame_equalities' ... /\ frame_equalities' .. /\ ...) == ?u,
  // with some frame_equalities' possibly already fully reduced
  // We repeatedly split the clause and extract the term on the left
  // to generate equalities on atomic subresources
  ignore (repeat (fun _ ->
    // Try to split the conjunction. If there is no conjunction, we exit the repeat
    apply_lemma (`elim_conjunction);
    // Dismiss the two uvars created for the RHS, they'll be solved by unification
    dismiss ();
    dismiss ();
    // The first goal is the left conjunction
    split ();
    // Removes the frame equality if it is about emp
    or_else (fun _ -> apply_lemma (`lemma_frame_emp); dismiss()) (fun _ -> ());
    // Rewrites the frame_equalities if it wasn't yet reduced
    or_else (fun _ -> apply_lemma (`lemma_frame_equalities); dismiss ()) (fun _ -> ());
    norm normal_steps;
    // Finally solve the uvar, finishing the rewriting for this clause
    trefl ()
  ));

  // Removes the frame equality if it is about emp
  or_else (fun _ -> apply_lemma (`lemma_frame_emp); dismiss()) (fun _ -> ());

  // We do not have conjunctions anymore, we try to apply the frame_equalities rewriting
  // If it fails, the frame was not symbolic, so there is nothing to do
  or_else (fun _ -> apply_lemma (`lemma_frame_equalities); dismiss ()) (fun _ -> ());
  norm normal_steps;
  trefl ())

[@@ __steel_reduce__]
unfold
let frame_equalities
  (frame:vprop)
  (h0:rmem frame) (h1:rmem frame) : prop
  = rewrite_with_tactic frame_vc_norm (frame_equalities' frame h0 h1)

/// More lemmas about the abstract can_be_split predicates, to be used as
/// rewriting rules in the tactic below
val can_be_split_dep_refl (p:vprop)
: Lemma (can_be_split_dep true_p p p)

val equiv_can_be_split (p1 p2:vprop) : Lemma
  (requires p1 `equiv` p2)
  (ensures p1 `can_be_split` p2)

val intro_can_be_split_frame (p q:vprop) (frame:vprop)
  : Lemma (requires q `equiv` (p `star` frame))
          (ensures can_be_split q p /\ True)

val can_be_split_post_elim (#a #b:Type) (t1:a -> post_t b) (t2:post_t b)
  : Lemma (requires (forall (x:a) (y:b). t1 x y `equiv` t2 y))
          (ensures t1 `can_be_split_post` t2)

val equiv_forall_refl (#a:Type) (t:post_t a)
  : Lemma (t `equiv_forall` t)

val equiv_forall_elim (#a:Type) (t1 t2:post_t a)
  : Lemma (requires (forall (x:a). t1 x `equiv` t2 x))
          (ensures t1 `equiv_forall` t2)

open FStar.Tactics.CanonCommMonoidSimple.Equiv

(* equiv is an equivalence relation on vprops *)

/// Lemmas establishing the equivalence properties on equiv
val equiv_refl (x:vprop) : Lemma (equiv x x)

val equiv_sym (x y:vprop) : Lemma
  (requires equiv x y)
  (ensures equiv y x)

val equiv_trans (x y z:vprop) : Lemma
  (requires equiv x y /\ equiv y z)
  (ensures equiv x z)

module CE = FStar.Algebra.CommMonoid.Equiv

/// Equiv is an equivalence relation for vprops elements
inline_for_extraction noextract let req : CE.equiv vprop =
  CE.EQ equiv
     equiv_refl
     equiv_sym
     equiv_trans

(* Star induces a commutative monoid for the equiv equivalence relation *)

/// Lemmas establishing the commutative monoid properties
val cm_identity (x:vprop) : Lemma ((emp `star` x) `equiv` x)

val star_commutative (p1 p2:vprop)
  : Lemma ((p1 `star` p2) `equiv` (p2 `star` p1))

val star_associative (p1 p2 p3:vprop)
  : Lemma (((p1 `star` p2) `star` p3)
           `equiv`
           (p1 `star` (p2 `star` p3)))

val star_congruence (p1 p2 p3 p4:vprop)
  : Lemma (requires p1 `equiv` p3 /\ p2 `equiv` p4)
          (ensures (p1 `star` p2) `equiv` (p3 `star` p4))

/// Star induces a commutative monoid on vprops
[@__steel_reduce__]
inline_for_extraction noextract let rm : CE.cm vprop req =
  CE.CM emp
     star
     cm_identity
     star_associative
     star_commutative
     star_congruence

(*** Vprop combinators ***)

(* Refining a vprop with a selector predicate *)

/// Separation logic predicate stating the validity of a vprop with an additional refinement on its selector
val vrefine_hp (v: vprop) (p: (normal (t_of v) -> Tot prop)) : Tot (slprop u#1)

/// Exposing the validity of the above predicate when needed for proof purposes
val interp_vrefine_hp (v: vprop) (p: (normal (t_of v) -> Tot prop)) (m: mem) : Lemma
  (interp (vrefine_hp v p) m <==> (interp (hp_of v) m /\ p (sel_of v m)))

/// Selector type for a refined vprop
[@__steel_reduce__]
let vrefine_t (v: vprop) (p: (normal (t_of v) -> Tot prop)) : Tot Type
= (x: t_of v {p x})

/// Selector of a refined vprop. Returns a value which satisfies the refinement predicate
val vrefine_sel (v: vprop) (p: (normal (t_of v) -> Tot prop)) : Tot (selector (vrefine_t v p) (vrefine_hp v p))

/// Exposing the definition of the refined selector
val vrefine_sel_eq (v: vprop) (p: (normal (t_of v) -> Tot prop)) (m: Mem.hmem (vrefine_hp v p)) : Lemma
  (
    interp (hp_of v) m /\
    vrefine_sel v p m == sel_of v m
  )
//  [SMTPat ((vrefine_sel v p) m)] // FIXME: this pattern causes Z3 "wrong number of argument" errors

/// Combining the above pieces to define a vprop refined by a selector prediacte
[@__steel_reduce__]
let vrefine' (v: vprop) (p: (normal (t_of v) -> Tot prop)) : Tot vprop' = {
  hp = vrefine_hp v p;
  t = vrefine_t v p;
  sel = vrefine_sel v p;
}
val vrefine : v: Steel.Effect.Common.vprop ->
    p: (_: Steel.Effect.Common.normal (Steel.Effect.Common.t_of v) -> Prims.prop)
  -> Steel.Effect.Common.vprop

    v: Steel.Effect.Common.vprop ->
    p: (_: Steel.Effect.Common.normal (Steel.Effect.Common.t_of v) -> Prims.prop)
  -> Steel.Effect.Common.vprop