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]
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
]
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
Prims.Cons FStar.Pervasives.norm_step FStar.Pervasives.delta_attr Prims.string Prims.Nil FStar.Pervasives.delta_only FStar.Pervasives.delta_qualifier FStar.Pervasives.iota FStar.Pervasives.zeta FStar.Pervasives.primops FStar.Pervasives.simplify
(*
   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
val normal_steps : Prims.list FStar.Pervasives.norm_step
Prims.list FStar.Pervasives.norm_step