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
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
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.post_t Prims.l_Forall Steel.Effect.Common.equiv_forall Prims.logical
(*
   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
val can_be_split_post : t1: (_: a -> Steel.Effect.Common.post_t b) -> t2: Steel.Effect.Common.post_t b -> Prims.logical
t1: (_: a -> Steel.Effect.Common.post_t b) -> t2: Steel.Effect.Common.post_t b -> Prims.logical