DM4Free Effect: "(Error 172) Tm_refine is outside of the definition language"

[azike]

Hi!
I have a question about an Error I encountered while trying to create a new effect.
Since I wanted to be able to do some extrinsic proofs (i.e. write a Lemma) and not only rely on intrinsic ones, I decided to use the DM effects, as I figured reify does not work well at the time for LayeredEffects?
Anyway, I wanted to use the example of the STATE_h Effect and embedded my own state type.
As I tried to compile, I got the error message: (Error 172) Tm_refine is outside of the definition language: ..., which I can not make sense of.
The state type I want to use is a refinement type (if that causes the problem).
I got the same error when using nat as state type as opposed to int (see below):

let st (s:Type) (a:Type) = s -> M (a * s)
let return_st (s:Type) (a:Type) (x:a) : st s a = fun s0 -> x, s0
let bind_st (s:Type) (a:Type) (b:Type) (f:st s a) (g:a -> st s b) : st s b
  = fun (s0:s) -> let (a,s) = f s0 in g a s

let get (s:Type) () : st s s = fun s0 -> s0, s0
let put (s:Type) (x:s) : st s unit = fun _ -> (), x

total reifiable reflectable new_effect {
  STATE_h (s:Type0) : a:Type -> Effect
  with repr     = st s
     ; bind     = bind_st s
     ; return   = return_st s
     ; get      = get s
     ; put      = put s
}

total reifiable reflectable new_effect STATE_NAT = STATE_h nat

(* 
Yields:
(Error 172) Tm_refine is outside of the definition language: i: Prims.int{x: Prims.unit{Prims.equals (i >= 0) true}}
 *)

I would appreciate if anybody could tell me what this error is all about.

Thank you in advance!

[nikswamy]

Hi,

The DM4Free feature comes with various limitations. In particular, the representation of the effect cannot use refinement types.

Your definition of STATE_h is parameterized by the type of the state and so does not violate the no-refinements constraints. But, when you instantiate it with nat, then indeed the no-refinements constraint is violated and F* complains.

You can still do this though:

total reifiable reflectable new_effect STATE_INT = STATE_h int

let test (x:int)
: STATE_INT int (fun s0 post -> s0 >= 0 /\ post (x, s0 + 1))
= let s = STATE_INT?.get () in
   let _ = STATE_INT?.put (s + 1) in
   x  

[azike]

Thanks for the answer!

I have two follow-up questions:

1. Would it also be possible to enforce the refinement via a new effect instead?
   Something like this:

effect State_Nat (a:Type) (pre) (post) =
   STATE_INT a (fun s0 p -> pre s0 /\ s0 >= 0 /\ (forall a s1.  post s0 a s1 ==> p (a ,s1)))

Otherwise, I would have to specify s0 >= 0 for every function.

2. Do you plan on supporting reify for Layered Effects in the near future?

Thank you very much!
br