val if_then_else_ens
      (#a: Type)
      (#pre_f #pre_g: pre_t)
      (#post_f #post_g: post_t a)
      (#frame_f #frame_g: vprop)
      (#pr: prop)
      (s1: squash (can_be_split_dep pr (pre_f `star` frame_f) (pre_g `star` frame_g)))
      (s2:
          squash (equiv_forall (fun x -> (post_f x) `star` frame_f)
                (fun x -> (post_g x) `star` frame_g)))
      (ens_then: ens_t pre_f a post_f)
      (ens_else: ens_t pre_g a post_g)
      (p: Type0)
    : ens_t (pre_f `star` frame_f) a (fun x -> (post_f x) `star` frame_f)
let if_then_else_ens (#a:Type)
  (#pre_f:pre_t) (#pre_g:pre_t) (#post_f:post_t a) (#post_g:post_t a)
  (#frame_f #frame_g:vprop) (#pr:prop)
  (s1: squash (can_be_split_dep pr (pre_f `star` frame_f) (pre_g `star` frame_g)))
  (s2: squash (equiv_forall (fun x -> post_f x `star` frame_f) (fun x -> post_g x `star` frame_g)))
  (ens_then:ens_t pre_f a post_f) (ens_else:ens_t pre_g a post_g)
  (p:Type0)
: ens_t (pre_f `star` frame_f) a (fun x -> post_f x `star` frame_f)
= fun h0 x h1 -> pr /\ (
    can_be_split_trans (pre_f `star` frame_f) (pre_g `star` frame_g) pre_g;
    can_be_split_trans (post_f x `star` frame_f) (post_g x `star` frame_g) (post_g x);
    (p ==> ens_then (focus_rmem h0 pre_f) x (focus_rmem h1 (post_f x))) /\
    ((~ p) ==> ens_else (focus_rmem h0 pre_g) x (focus_rmem h1 (post_g x))))
val if_then_else_ens
      (#a: Type)
      (#pre_f #pre_g: pre_t)
      (#post_f #post_g: post_t a)
      (#frame_f #frame_g: vprop)
      (#pr: prop)
      (s1: squash (can_be_split_dep pr (pre_f `star` frame_f) (pre_g `star` frame_g)))
      (s2:
          squash (equiv_forall (fun x -> (post_f x) `star` frame_f)
                (fun x -> (post_g x) `star` frame_g)))
      (ens_then: ens_t pre_f a post_f)
      (ens_else: ens_t pre_g a post_g)
      (p: Type0)
    : ens_t (pre_f `star` frame_f) a (fun x -> (post_f x) `star` frame_f)
let if_then_else_ens
      (#a: Type)
      (#pre_f #pre_g: pre_t)
      (#post_f #post_g: post_t a)
      (#frame_f #frame_g: vprop)
      (#pr: prop)
      (s1: squash (can_be_split_dep pr (pre_f `star` frame_f) (pre_g `star` frame_g)))
      (s2:
          squash (equiv_forall (fun x -> (post_f x) `star` frame_f)
                (fun x -> (post_g x) `star` frame_g)))
      (ens_then: ens_t pre_f a post_f)
      (ens_else: ens_t pre_g a post_g)
      (p: Type0)
    : ens_t (pre_f `star` frame_f) a (fun x -> (post_f x) `star` frame_f) =
fun h0 x h1 ->
  pr /\
  (can_be_split_trans (pre_f `star` frame_f) (pre_g `star` frame_g) pre_g;
    can_be_split_trans ((post_f x) `star` frame_f) ((post_g x) `star` frame_g) (post_g x);
    (p ==> ens_then (focus_rmem h0 pre_f) x (focus_rmem h1 (post_f x))) /\
    ((~p) ==> ens_else (focus_rmem h0 pre_g) x (focus_rmem h1 (post_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.vprop Prims.prop Prims.squash Steel.Effect.Common.can_be_split_dep Steel.Effect.Common.star Steel.Effect.Common.equiv_forall Steel.Effect.Common.ens_t Steel.Effect.Common.rmem Prims.l_and Prims.l_imp Steel.Effect.Common.focus_rmem Prims.l_not 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)))
: 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))))

/// Logical postcondition for the composition (bind) of two Steel computations:
/// The precondition of the first computation was satisfied in the initial state, and there
/// exists an intermediate state where the two-state postcondition of the first computation was
/// satisfied, and which yields the validity of the two-state postcondition of the second computation
/// on the final state [m2] with the returned value [y]

/// Note that the ensures for the bind below asserts req_f
/// This is not necessary, but an explicit assert may help the solver

unfold
let bind_ens (#a:Type) (#b: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) (#post_g:a -> post_t b)
  (#pr:a -> prop)
  (ens_g:(x:a -> ens_t (pre_g x) b (post_g x)))
  (frame_f:vprop) (frame_g:a -> vprop)
  (post:post_t b)
  (_:squash (can_be_split_forall_dep pr (fun x -> post_f x `star` frame_f) (fun x -> pre_g x `star` frame_g x)))
  (_:squash (can_be_split_post (fun x y -> post_g x y `star` frame_g x) post))
: ens_t (pre_f `star` frame_f) b post
= fun m0 y m2 ->
  req_f (focus_rmem m0 pre_f) /\
  (exists (x:a) (h1:hmem (post_f x `star` frame_f)).
    pr x /\
    (
    can_be_split_trans (post_f x `star` frame_f) (pre_g x `star` frame_g x) (pre_g x);
    can_be_split_trans (post_f x `star` frame_f) (pre_g x `star` frame_g x) (frame_g x);
    can_be_split_trans (post y) (post_g x y `star` frame_g x) (post_g x y);
    can_be_split_trans (post y) (post_g x y `star` frame_g x) (frame_g x);
    frame_equalities frame_f (focus_rmem m0 frame_f) (focus_rmem (mk_rmem (post_f x `star` frame_f) h1) frame_f) /\
    frame_equalities (frame_g x) (focus_rmem (mk_rmem (post_f x `star` frame_f) h1) (frame_g x)) (focus_rmem m2 (frame_g x)) /\
    ens_f (focus_rmem m0 pre_f) x (focus_rmem (mk_rmem (post_f x `star` frame_f) h1) (post_f x)) /\
    (ens_g x) (focus_rmem (mk_rmem (post_f x `star` frame_f) h1) (pre_g x)) y (focus_rmem m2 (post_g x y))))

/// Steel effect combinator to compose two Steel computations
/// Separation logic VCs are squashed goals passed as implicits, annotated with the framing_implicit
/// attribute. This indicates that they will be discharged by the tactic in Steel.Effect.Common
/// Requires/ensures logical VCs are defined using weakest preconditions combinators defined above,
/// and discharged by SMT.
val bind (a:Type) (b:Type)
  (#framed_f:eqtype_as_type bool)
  (#framed_g:eqtype_as_type bool)
  (#[@@@ framing_implicit] pre_f:pre_t) (#[@@@ framing_implicit] post_f:post_t a)
  (#[@@@ framing_implicit] req_f:req_t pre_f) (#[@@@ framing_implicit] ens_f:ens_t pre_f a post_f)
  (#[@@@ framing_implicit] pre_g:a -> pre_t) (#[@@@ framing_implicit] post_g:a -> post_t b)
  (#[@@@ framing_implicit] req_g:(x:a -> req_t (pre_g x))) (#[@@@ framing_implicit] ens_g:(x:a -> ens_t (pre_g x) b (post_g x)))
  (#[@@@ framing_implicit] frame_f:vprop) (#[@@@ framing_implicit] frame_g:a -> vprop)
  (#[@@@ framing_implicit] post:post_t b)
  (#[@@@ framing_implicit] _ : squash (maybe_emp framed_f frame_f))
  (#[@@@ framing_implicit] _ : squash (maybe_emp_dep framed_g frame_g))
  (#[@@@ framing_implicit] pr:a -> prop)
  (#[@@@ framing_implicit] p1:squash (can_be_split_forall_dep pr
    (fun x -> post_f x `star` frame_f) (fun x -> pre_g x `star` frame_g x)))
  (#[@@@ framing_implicit] p2:squash (can_be_split_post (fun x y -> post_g x y `star` frame_g x) post))
  (f:repr a framed_f pre_f post_f req_f ens_f)
  (g:(x:a -> repr b framed_g (pre_g x) (post_g x) (req_g x) (ens_g x)))
: repr b
    true
    (pre_f `star` frame_f)
    post
    (bind_req req_f ens_f req_g frame_f frame_g p1)
    (bind_ens req_f ens_f ens_g frame_f frame_g post p1 p2)

/// Logical precondition for subtyping relation for Steel computation.
unfold
let subcomp_pre (#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:pre_t) (#post_g:post_t a) (req_g:req_t pre_g) (ens_g:ens_t pre_g a post_g)
  (#frame:vprop)
  (#pr:prop)
  (_:squash (can_be_split_dep pr pre_g (pre_f `star` frame)))
  (_:squash (equiv_forall post_g (fun x -> post_f x `star` frame)))
  : pure_pre
// The call to with_tactic allows us to reduce VCs in a controlled way, once all
// uvars have been resolved.
// To ensure an SMT-friendly encoding of the VC, it needs to be encapsulated in a squash call
= T.rewrite_with_tactic vc_norm (squash (
  (forall (h0:hmem pre_g). req_g (mk_rmem pre_g h0) ==> pr /\
    (can_be_split_trans pre_g (pre_f `star` frame) pre_f;
    req_f (focus_rmem (mk_rmem pre_g h0) pre_f))) /\
  (forall (h0:hmem pre_g) (x:a) (h1:hmem (post_g x)). (
     pr ==> (
     can_be_split_trans (post_g x) (post_f x `star` frame) (post_f x);
     can_be_split_trans (pre_g) (pre_f `star` frame) frame;
     can_be_split_trans (post_g x) (post_f x `star` frame) frame;
     can_be_split_trans pre_g (pre_f `star` frame) pre_f;

     (req_g (mk_rmem pre_g h0) /\
      ens_f (focus_rmem (mk_rmem pre_g h0) pre_f) x (focus_rmem (mk_rmem (post_g x) h1) (post_f x)) /\
      frame_equalities frame
        (focus_rmem (mk_rmem pre_g h0) frame)
        (focus_rmem (mk_rmem (post_g x) h1) frame))

        ==> ens_g (mk_rmem pre_g h0) x (mk_rmem (post_g x) h1))
  ))
))

/// Subtyping combinator for Steel computations.
/// Computation [f] is given type `repr a framed_g pre_g post_g req_g ens_g`.
/// As for bind, separation logic goals are encoded as squashed implicits which will be discharged
/// by tactic, while logical requires/ensures operating on selectors are discharged by SMT
val subcomp (a:Type)
  (#framed_f:eqtype_as_type bool)
  (#framed_g:eqtype_as_type bool)
  (#[@@@ framing_implicit] pre_f:pre_t) (#[@@@ framing_implicit] post_f:post_t a)
  (#[@@@ framing_implicit] req_f:req_t pre_f) (#[@@@ framing_implicit] ens_f:ens_t pre_f a post_f)
  (#[@@@ framing_implicit] pre_g:pre_t) (#[@@@ framing_implicit] post_g:post_t a)
  (#[@@@ framing_implicit] req_g:req_t pre_g) (#[@@@ framing_implicit] ens_g:ens_t pre_g a post_g)
  (#[@@@ framing_implicit] frame:vprop)
  (#[@@@ framing_implicit] _ : squash (maybe_emp framed_f frame))
  (#[@@@ framing_implicit] pr : prop)
  (#[@@@ framing_implicit] p1:squash (can_be_split_dep pr pre_g (pre_f `star` frame)))
  (#[@@@ framing_implicit] p2:squash (equiv_forall post_g (fun x -> post_f x `star` frame)))
  (f:repr a framed_f pre_f post_f req_f ens_f)
: Pure (repr a framed_g pre_g post_g req_g ens_g)
  (requires subcomp_pre req_f ens_f req_g ens_g p1 p2)
  (ensures fun _ -> True)

/// Logical precondition for the if_then_else combinator
unfold
let if_then_else_req
  (#pre_f:pre_t) (#pre_g:pre_t) (#frame_f #frame_g:vprop) (#pr: prop)
  (s_pre: squash (can_be_split_dep pr (pre_f `star` frame_f) (pre_g `star` frame_g)))
  (req_then:req_t pre_f) (req_else:req_t pre_g)
  (p:Type0)
: req_t (pre_f `star` frame_f)
= fun h -> pr /\ (
    can_be_split_trans (pre_f `star` frame_f) (pre_g `star` frame_g) pre_g;
    (p ==> req_then (focus_rmem h pre_f)) /\
    ((~ p) ==> req_else (focus_rmem h pre_g)))

/// Logical postcondition for the if_then_else combinator
unfold
let if_then_else_ens (#a:Type)
  (#pre_f:pre_t) (#pre_g:pre_t) (#post_f:post_t a) (#post_g:post_t a)
  (#frame_f #frame_g:vprop) (#pr:prop)
  (s1: squash (can_be_split_dep pr (pre_f `star` frame_f) (pre_g `star` frame_g)))
  (s2: squash (equiv_forall (fun x -> post_f x `star` frame_f) (fun x -> post_g x `star` frame_g)))
  (ens_then:ens_t pre_f a post_f) (ens_else:ens_t pre_g a post_g)
  (p:Type0)
val if_then_else_ens
      (#a: Type)
      (#pre_f #pre_g: pre_t)
      (#post_f #post_g: post_t a)
      (#frame_f #frame_g: vprop)
      (#pr: prop)
      (s1: squash (can_be_split_dep pr (pre_f `star` frame_f) (pre_g `star` frame_g)))
      (s2:
          squash (equiv_forall (fun x -> (post_f x) `star` frame_f)
                (fun x -> (post_g x) `star` frame_g)))
      (ens_then: ens_t pre_f a post_f)
      (ens_else: ens_t pre_g a post_g)
      (p: Type0)
    : ens_t (pre_f `star` frame_f) a (fun x -> (post_f x) `star` frame_f)

    s1:
      Prims.squash (Steel.Effect.Common.can_be_split_dep pr
            (Steel.Effect.Common.star pre_f frame_f)
            (Steel.Effect.Common.star pre_g frame_g)) ->
    s2:
      Prims.squash (Steel.Effect.Common.equiv_forall (fun x ->
                Steel.Effect.Common.star (post_f x) frame_f)
            (fun x -> Steel.Effect.Common.star (post_g x) frame_g)) ->
    ens_then: Steel.Effect.Common.ens_t pre_f a post_f ->
    ens_else: Steel.Effect.Common.ens_t pre_g a post_g ->
    p: Type0
  -> Steel.Effect.Common.ens_t (Steel.Effect.Common.star pre_f frame_f)
      a
      (fun x -> Steel.Effect.Common.star (post_f x) frame_f)