dm4f: M not quite a synonym for Tot

[catalin-hritcu]

Switching from Tot to M causes 3 of my previous ifc proofs to fail. For instance, the following code works with Tot, but does not work with M:

module Bug

type label =
  | Low
  | High

let ifc (a:Type) = label -> M (option (a * label))

let eq_ifc (a:Type) (f:ifc a) (g:ifc a) =
   forall l. f l == g l

let return_ifc (a:Type) (x:a) : ifc a = fun l -> Some (x, l)
let bind_ifc (a:Type) (b:Type) (f:ifc a) (g: a -> Tot (ifc b)) : ifc b
  = fun l0 -> let fl0 = f l0 in match fl0 with
           | None -> None
           | Some (x, l1) ->
             let gxl1 = g x l1 in match gxl1 with
             | None -> None
             | Some (y, l2) -> Some(y, l2)

val left_unit: a:Type -> b:Type -> x:a -> f:(a -> Tot (ifc b))
            -> Lemma (eq_ifc b (bind_ifc a b (return_ifc a x) f) (f x))
let left_unit a b x f = ()

[hritcu@detained bug-reports]$ fstar.exe bug710.fst
./bug710.fst(22,71-23,26): could not prove post-condition
Error: 1 errors were reported (see above)

[catalin-hritcu]

@kyoDralliam was looking at this and it seems a problem with the way M is encoded to the SMT solver.

[kyoDralliam]

More precisely, M is encoded in the SMT solver query as a non total effect.

[kyoDralliam]

Fixed by the introduction of the cps attribute (commit 9168f97)

[catalin-hritcu]

If this is fixed we should consider moving the monad laws from
https://github.com/FStarLang/FStar/blob/master/examples/dm4free/FStar.DM4F.MonadLaws.fst
to their respective files and make them use M instead of Tot.