val ni : f: (_: Prims.unit -> IfcDeclassify.St Prims.unit) -> Type0
let ni (f:unit -> St unit) = (s:rel state) ->
  Lemma (requires (low_equiv s))
        (ensures (let sl = snd (reify (f ()) (R?.l s)) in
                  let sr = snd (reify (f ()) (R?.r s)) in
                  (sl.release \/ sr.release \/ low_equiv (R sl sr))))
(*
   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 IfcDeclassify

open FStar.DM4F.ST
open Rel

(* Simple example illustrating an IFC property that needs to be stated
   in terms of an instrumented monad. *)

(* We define a variant of the state effect where the state has 3 fields:
   - a secret integer cell
   - a public integer cell
   - a boolean: when this is set the secret integer is declassified
                and allowed to leak to the public cell *)

type state = {secret:int;
              public:int;
              release:bool}

(* Instantiating the effect template in FStar.DM4F.ST leads to universe issues *)
total reifiable reflectable new_effect {
  STATE  : a:Type -> Effect
  with repr     = st state
     ; bind     = bind_st state
     ; return   = return_st state
     ; get      = get state
     ; put      = put state
}


effect ST (a:Type) (pre: STATE?.pre) (post: (state -> a -> state -> GTot Type0)) =
  STATE a (fun n0 p -> pre n0 /\
            (forall a n1. pre n0 /\ post n0 a n1 ==> p (a, n1)))

effect St (a:Type) =
  STATE a (fun (_:state) (p:(a * state) -> Type0) -> forall (x:(a * state)). p x)

(* equivalence *)

type low_equiv (s : rel state) = (R?.l s).public == (R?.r s).public
/
Rel.fst.checked prims.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.DM4F.ST.fst.checked
IfcDeclassify.fst
f: (_: Prims.unit -> IfcDeclassify.St Prims.unit) -> Type0
Prims.unit Rel.rel IfcDeclassify.state IfcDeclassify.low_equiv Prims.squash Prims.l_or Prims.b2t IfcDeclassify.__proj__Mkstate__item__release Rel.R FStar.Pervasives.Native.snd Rel.__proj__R__item__r Rel.__proj__R__item__l Prims.Nil FStar.Pervasives.pattern
let ni (f: (unit -> St unit)) =
  
s: rel state
  -> Lemma (requires (low_equiv s))
      (ensures
        (let sl = snd (reify (f ()) (R?.l s)) in
          let sr = snd (reify (f ()) (R?.r s)) in
          (sl.release \/ sr.release \/ low_equiv (R sl sr))))