val witnessed_impl (p q: s_pred)
    : Lemma ((witnessed (fun s -> p s ==> q s) /\ witnessed p) ==> witnessed q)
val witnessed_impl (p q: s_pred)
    : Lemma ((witnessed (fun s -> p s ==> q s) /\ witnessed p) ==> witnessed q)
let witnessed_impl (p q:s_pred)
: Lemma ((witnessed (fun s -> p s ==> q s) /\ witnessed p) ==> witnessed q)
= W.lemma_witnessed_impl grows p q
(*
   Copyright 2008-2018 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 MSeqExn

module W = FStar.Monotonic.Witnessed

/// This module provides a monotonic state + exception layered effect,
/// where state is a monotonic sequence of events


module Seq = FStar.Seq


/// The event type, it can be in any fixed universe

assume type event : Type u#1


/// An invariant that the monotonic sequence must maintain

assume type invariant (s:Seq.seq event) : Type0


/// state is a sequence of events that holds the invariant

type state = s:Seq.seq event{invariant s}


/// The result type for the exceptions

type result (a:Type) =
  | Success : a -> result a
  | Error   : string -> result a


/// The state grows monotonically

let grows : Preorder.preorder state =
  fun s1 s2 ->
  Seq.length s1 <= Seq.length s2 /\
  (forall (i:nat).{:pattern (Seq.index s1 i) \/ (Seq.index s2 i)}
            i < Seq.length s1 ==> Seq.index s1 i == Seq.index s2 i)


/// Now into the effect mechanics

type pre_t = state -> Type0
type post_t (a:Type) = result a -> state -> Type0
type wp_t0 (a:Type) = post_t a -> pre_t

unfold
let wpt_monotonic (#a:Type) (wp:wp_t0 a) =
  forall (p q:post_t a).
    (forall (r:result a) (s:state). p r s ==> q r s) ==>
    (forall (s:state). wp p s ==> wp q s)

type wp_t (a:Type) = wp:wp_t0 a{wpt_monotonic wp}

open FStar.Monotonic.Pure

let repr (a:Type) (wp:wp_t a) =
  s0:state ->
  PURE (result a & state)
    (as_pure_wp (fun p -> wp (fun x s1 -> grows s0 s1 ==> p (x, s1)) s0))

let return (a:Type) (x:a)
: repr a (fun p s0 -> p (Success x) s0)
= fun s0 -> Success x, s0

let bind (a:Type) (b:Type)
  (wp_f:wp_t a) (wp_g:a -> wp_t b)
  (f:repr a wp_f) (g:(x:a -> repr b (wp_g x)))
: repr b
  (fun p -> wp_f (fun x ->
   match x with
   | Error e -> p (Error e)
   | Success x -> (wp_g x) p))
= fun s0 ->
  let x, s1 = f s0 in
  match x with
  | Error e -> Error e, s1
  | Success x -> (g x) s1

let subcomp (a:Type)
  (wp_f:wp_t a) (wp_g:wp_t a)
  (f:repr a wp_f)
: Pure (repr a wp_g)
  (requires forall p s. wp_g p s ==> wp_f p s)
  (ensures fun _ -> True)
= f

let if_then_else (a:Type)
  (wp_then:wp_t a) (wp_else:wp_t a)
  (f:repr a wp_then) (g:repr a wp_else)
  (p:bool)
: Type
= repr a
  (fun post s0 ->
    (p ==> wp_then post s0) /\
    ((~ p) ==> wp_else post s0))

reifiable reflectable
effect {
  MSeqEXN (a:Type) (_:wp_t a)
  with {repr; return; bind; subcomp; if_then_else}
}

unfold
let lift_pure_wp (#a:Type) (wp:pure_wp a) : wp_t a =
  FStar.Monotonic.Pure.elim_pure_wp_monotonicity wp;
  fun p s0 -> wp (fun x -> p (Success x) s0)

let lift_pure_mseqexn (a:Type) (wp:pure_wp a) (f:unit -> PURE a wp)
: repr a (lift_pure_wp wp)
= elim_pure_wp_monotonicity_forall (); fun s0 -> Success (f ()), s0

sub_effect PURE ~> MSeqEXN = lift_pure_mseqexn

effect MSeqExn (a:Type) (req:state -> Type0) (ens:(state -> result a -> state -> Type0)) =
  MSeqEXN a (fun post s0 -> req s0 /\ (forall (x:result a) (s1:state). ens s0 x s1 ==> post x s1))


/// witness and recall of stable predicates

type s_pred = state -> Type0

let stable (p:s_pred) =
  forall s0 s1. (p s0 /\ grows s0 s1) ==> p s1

let witnessed (p:s_pred) = W.witnessed grows p

assume val witness (p:s_pred)
: MSeqExn unit
  (fun s0 -> p s0 /\ stable p)
  (fun s0 r s1 -> r == Success () /\ s0 == s1 /\ witnessed p)

assume val recall (p:s_pred)
: MSeqExn unit
  (fun _ -> witnessed p)
  (fun s0 r s1 -> r == Success () /\ s0 == s1 /\ p s0)

let witnessed_constant (p:Type0)
: Lemma (witnessed (fun _ -> p) <==> p)
= W.lemma_witnessed_constant grows p

let witnessed_nested (p:s_pred)
: Lemma (witnessed (fun s -> witnessed p) <==> witnessed p)
= assert_norm (witnessed (fun _ -> witnessed p) ==
               W.witnessed grows (fun _ -> W.witnessed grows p));
  assert_norm (witnessed p == W.witnessed grows p);
  W.lemma_witnessed_nested grows p

let witnessed_and (p q:s_pred)
: Lemma (witnessed (fun s -> p s /\ q s) <==> (witnessed p /\ witnessed q))
= W.lemma_witnessed_and grows p q

let witnessed_or (p q:s_pred)
: Lemma ((witnessed p \/ witnessed q) ==> witnessed (fun s -> p s \/ q s))
= W.lemma_witnessed_or grows p q
/
prims.fst.checked FStar.Seq.fst.checked FStar.Preorder.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Monotonic.Witnessed.fsti.checked FStar.Monotonic.Pure.fst.checked
MSeqExn.fst
p: MSeqExn.s_pred -> q: MSeqExn.s_pred
  -> FStar.Pervasives.Lemma
    (ensures MSeqExn.witnessed (fun s -> p s ==> q s) /\ MSeqExn.witnessed p ==> MSeqExn.witnessed q
    )
MSeqExn.s_pred FStar.Monotonic.Witnessed.lemma_witnessed_impl MSeqExn.state MSeqExn.grows Prims.unit Prims.l_True Prims.squash Prims.l_imp Prims.l_and MSeqExn.witnessed Prims.Nil FStar.Pervasives.pattern
let witnessed_impl (p q: s_pred)
    : Lemma ((witnessed (fun s -> p s ==> q s) /\ witnessed p) ==> witnessed q) =
  
W.lemma_witnessed_impl grows p q