val bind_req:
    #a: Type ->
    #pre_f: pre_t ->
    #post_f: post_t a ->
    req_f: req_t pre_f ->
    ens_f: ens_t pre_f a post_f ->
    #pre_g: (a -> pre_t) ->
    #pr: (a -> prop) ->
    req_g: (x: a -> req_t (pre_g x)) ->
    frame_f: vprop ->
    frame_g: (a -> vprop) ->
    squash (can_be_split_forall_dep pr
            (fun x -> (post_f x) `star` frame_f)
            (fun x -> (pre_g x) `star` (frame_g x)))
  -> req_t (pre_f `star` frame_f)
let bind_req (#a:Type)
  (#pre_f:pre_t) (#post_f:post_t a)
  (req_f:req_t pre_f) (ens_f:ens_t pre_f a post_f)
  (#pre_g:a -> pre_t)
  (#pr:a -> prop)
  (req_g:(x:a -> req_t (pre_g x)))
  (frame_f:vprop) (frame_g:a -> vprop)
  (_:squash (can_be_split_forall_dep pr (fun x -> post_f x `star` frame_f) (fun x -> pre_g x `star` frame_g x)))
: req_t (pre_f `star` frame_f)
= fun m0 ->
  req_f (focus_rmem m0 pre_f) /\
  (forall (x:a) (h1:hmem (post_f x `star` frame_f)).
    (ens_f (focus_rmem m0 pre_f) x (focus_rmem (mk_rmem (post_f x `star` frame_f) h1) (post_f x)) /\
      frame_equalities frame_f (focus_rmem m0 frame_f) (focus_rmem (mk_rmem (post_f x `star` frame_f) h1) frame_f))
    ==> pr x /\
      (can_be_split_trans (post_f x `star` frame_f) (pre_g x `star` frame_g x) (pre_g x);
      (req_g x) (focus_rmem (mk_rmem (post_f x `star` frame_f) h1) (pre_g x))))
val bind_req:
    #a: Type ->
    #pre_f: pre_t ->
    #post_f: post_t a ->
    req_f: req_t pre_f ->
    ens_f: ens_t pre_f a post_f ->
    #pre_g: (a -> pre_t) ->
    #pr: (a -> prop) ->
    req_g: (x: a -> req_t (pre_g x)) ->
    frame_f: vprop ->
    frame_g: (a -> vprop) ->
    squash (can_be_split_forall_dep pr
            (fun x -> (post_f x) `star` frame_f)
            (fun x -> (pre_g x) `star` (frame_g x)))
  -> req_t (pre_f `star` frame_f)
let bind_req
      (#a: Type)
      (#pre_f: pre_t)
      (#post_f: post_t a)
      (req_f: req_t pre_f)
      (ens_f: ens_t pre_f a post_f)
      (#pre_g: (a -> pre_t))
      (#pr: (a -> prop))
      (req_g: (x: a -> req_t (pre_g x)))
      (frame_f: vprop)
      (frame_g: (a -> vprop))
      (_:
          squash (can_be_split_forall_dep pr
                (fun x -> (post_f x) `star` frame_f)
                (fun x -> (pre_g x) `star` (frame_g x))))
    : req_t (pre_f `star` frame_f) =
fun m0 ->
  req_f (focus_rmem m0 pre_f) /\
  (forall (x: a) (h1: hmem ((post_f x) `star` frame_f)).
      (ens_f (focus_rmem m0 pre_f)
          x
          (focus_rmem (mk_rmem ((post_f x) `star` frame_f) h1) (post_f x)) /\
        frame_equalities frame_f
          (focus_rmem m0 frame_f)
          (focus_rmem (mk_rmem ((post_f x) `star` frame_f) h1) frame_f)) ==>
      pr x /\
      (can_be_split_trans ((post_f x) `star` frame_f) ((pre_g x) `star` (frame_g x)) (pre_g x);
        (req_g x) (focus_rmem (mk_rmem ((post_f x) `star` frame_f) h1) (pre_g x))))
Steel.Effect.fsti.checked
Steel.Memory.fsti.checked Steel.Effect.Common.fsti.checked prims.fst.checked FStar.Tactics.fst.checked FStar.Set.fsti.checked FStar.Pervasives.fsti.checked FStar.Ghost.fsti.checked FStar.FunctionalExtensionality.fsti.checked
Steel.Effect.fsti
Steel.Effect.Common.pre_t Steel.Effect.Common.post_t Steel.Effect.Common.req_t Steel.Effect.Common.ens_t Prims.prop Steel.Effect.Common.vprop Prims.squash Steel.Effect.Common.can_be_split_forall_dep Steel.Effect.Common.star Steel.Effect.Common.rmem Prims.l_and Steel.Effect.Common.focus_rmem Prims.l_Forall Steel.Effect.Common.hmem Prims.l_imp Steel.Effect.Common.mk_rmem Steel.Effect.Common.frame_equalities Prims.unit Steel.Effect.Common.can_be_split_trans
(*
   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

open Steel.Memory
module Mem = Steel.Memory
module FExt = FStar.FunctionalExtensionality
open FStar.Ghost
module T = FStar.Tactics

include Steel.Effect.Common

/// This module defines the main Steel effect, with requires and ensures predicates operating on
/// selectors, which will be discharged by SMT

#set-options "--warn_error -330"  //turn off the experimental feature warning
#set-options "--ide_id_info_off"

(* Defining the Steel effect with selectors *)

/// The underlying representation of Steel computations.
/// The framed bit indicates whether this computation has already been framed. This corresponds to the |- and |-_F modalities
/// in the ICFP21 paper
val repr (a:Type) (framed:bool) (pre:pre_t) (post:post_t a) (req:req_t pre) (ens:ens_t pre a post) : Type u#2

/// Logical precondition of the return combinator
unfold
let return_req (p:vprop) : req_t p = fun _ -> True

/// Logical postcondition of the return combinator:
/// The returned value [r] corresponds to the value passed to the return [x],
/// and return leaves selectors of all resources in [p] unchanged
unfold
let return_ens (a:Type) (x:a) (p:a -> vprop) : ens_t (p x) a p =
  fun (h0:rmem (p x)) (r:a) (h1:rmem (p r)) ->
    r == x /\ frame_equalities (p x) h0 (focus_rmem h1 (p x))

/// Monadic return combinator for the Steel effect. It is parametric in the postcondition
/// The vprop precondition is annotated with the return_pre predicate to enable special handling,
/// as explained in Steel.Effect.Common
val return_ (a:Type) (x:a) (#[@@@ framing_implicit] p:a -> vprop)
: repr a true (return_pre (p x)) p (return_req (p x)) (return_ens a x p)

/// Logical precondition for the composition (bind) of two Steel computations:
/// The postcondition of the first computation must imply the precondition of the second computation,
/// and also ensure that any equalities abducted during frame inference inside the predicate [pr] are satisfied
unfold
let bind_req (#a:Type)
  (#pre_f:pre_t) (#post_f:post_t a)
  (req_f:req_t pre_f) (ens_f:ens_t pre_f a post_f)
  (#pre_g:a -> pre_t)
  (#pr:a -> prop)
  (req_g:(x:a -> req_t (pre_g x)))
  (frame_f:vprop) (frame_g:a -> vprop)
  (_:squash (can_be_split_forall_dep pr (fun x -> post_f x `star` frame_f) (fun x -> pre_g x `star` frame_g x)))
val bind_req:
    #a: Type ->
    #pre_f: pre_t ->
    #post_f: post_t a ->
    req_f: req_t pre_f ->
    ens_f: ens_t pre_f a post_f ->
    #pre_g: (a -> pre_t) ->
    #pr: (a -> prop) ->
    req_g: (x: a -> req_t (pre_g x)) ->
    frame_f: vprop ->
    frame_g: (a -> vprop) ->
    squash (can_be_split_forall_dep pr
            (fun x -> (post_f x) `star` frame_f)
            (fun x -> (pre_g x) `star` (frame_g x)))
  -> req_t (pre_f `star` frame_f)

    req_f: Steel.Effect.Common.req_t pre_f ->
    ens_f: Steel.Effect.Common.ens_t pre_f a post_f ->
    req_g: (x: a -> Steel.Effect.Common.req_t (pre_g x)) ->
    frame_f: Steel.Effect.Common.vprop ->
    frame_g: (_: a -> Steel.Effect.Common.vprop) ->
    _:
      Prims.squash (Steel.Effect.Common.can_be_split_forall_dep pr
            (fun x -> Steel.Effect.Common.star (post_f x) frame_f)
            (fun x -> Steel.Effect.Common.star (pre_g x) (frame_g x)))
  -> Steel.Effect.Common.req_t (Steel.Effect.Common.star pre_f frame_f)