Interaction between reification and refinements yields inconsistency

[s-zanella]

I'm not sure what's the problem. F* doesn't give any warning.

$ fstar.exe M.fst 
Verified module: M (1095 milliseconds)
All verification conditions discharged successfully

module M

type store a = int -> M (a * int)

let return (a:Type) (x:a) : store a = fun h -> x, h

let bind (a b:Type) (m:store a) (f:a -> store b) : store b = fun h0 ->
  let z, h1 = m h0 in
  f z h1

let get () : store int = fun h -> h, h

reifiable new_effect_for_free {
  STORE: a:Type -> Effect
  with repr   = store
     ; bind   = bind
     ; return = return
  and effect_actions
       get    = get
}

let weird () : Lemma False =
  let _ = reify (STORE?.get () <: pos) 1 in
  ()

[catalin-hritcu]

It seems that this bug only affects the c_relational-ci_r3 branch. Should fix before merging into master.

[kyoDralliam]

This bug has been reported 2 weeks ago by @aseemr and debugged by @nikswamy. The problem comes from the fact that I disregarded the absence of subtyping for pairs as an implementation detail when I proposed a simpler rule for subtyping of DM4F computation. The result is that we currently do allow some subtyping for pairs in reified computation and we don't account for that in the smt-encoding. The culprit is just below :

(= (Prims.Mktuple2 Prims.pos Prims.int (BoxInt 1) (BoxInt 1))
   (ApplyTT (Test.__proj__STORE__item__get Tm_unit) (BoxInt 1)))

where the second line returns Prims.Mktuple2 Prims.Int Prims.Int (BoxInt 1) (BoxInt 1) and it results in equating int with nat which allows the smt to prove for example that 0 < -1 and inconsistency ensues.

The 2 ways out that we discussed with @aseemr and @nikswamy are :

• reverting the subtyping rule for DM4F computations since it is assuming subtyping for pairs which we do not have
• modify the encoding so that datatypes (in particular pairs) are not injective on their indices

@nikswamy began working on these but I don't know what's the current status

[s-zanella]

Sorry, I didn't notice the original report. So this new rule is in c_relational-ci_r3 but not in master, or why the difference between the branches?

I guess that removing the subtyping rule for DM4F is going to be less disruptive than modifying the encoding of indexed types.

[kyoDralliam]

There was no official report. The difference between the 2 branches is that c_relational-ci_r3 has the modifications at the encoding level to be able to do reasoning on reified term whereas on master reifed terms are often left as opaque impure value (so you cannot prove much about them).

Also there is an interesting similarity between this bug and the failure of subject reduction reported by Z. Luo in Universes in type theory (where he explains that subsumptive subtyping (what we have in F*) is badly behaving with MLTT-like type theories)

[nikswamy]

I have a couple of branches in various stages of completion trying to resolve this, together with the long-standing #349. It's high on my list of priorities. This is also related to #65, that addition of which will also solve this problem.

[nikswamy]

I have a tentative fix pushed and awaiting regressions.

Consider:

module Test
let st (a:Type) = int -> M (a * int)
let ret (a:Type) (x:a) : st a = fun (s:int) -> x, s
let bind (a:Type) (b:Type)
         (t1:st a)
         (t2:a -> st b)
    : st b
    = fun p ->
        let x, q = t1 p in
        t2 x q
let get () : st int = fun s0 -> s0, s0
reifiable new_effect_for_free {
  ST : a:Type -> Effect
  with repr     = st
     ; bind     = bind
     ; return   = ret
  and effect_actions
       get      = get
}
effect St (a:Type) = ST a (fun i post -> forall j. post j)

reifiable
let test_subtyping () : St nat =op_Multiply (ST?.get ()) (ST?.get ())

let bad (m:int{m = -1}) =
  let x = reify (test_subtyping ()) 0 in
  assert (x === Mktuple2 #int #int (fst x) (snd x));
  assert (int == nat);
  assert (m >= 0);
  assert False

This would incorrectly succeed, the proof of bad indicating where the problem lies, i.e., the implicit use of covariant subtyping on tuples, which is inconsistent with the rest of the SMT encoding.

With the revised subtyping rule from b3b7f3d, you have to write

reifiable
let test_subtyping () : St nat = let x = ST?.get () in let y = ST?.get() in op_Multiply x y

Or, of course:

reifiable
let test_subtyping () : St nat = let x = ST?.get () in op_Multiply x x

The point is that op_Multiply (get()) (get()) has type St int, because of the type of op_Multiply. And, since St is reifiable, you cannot directly use subtyping on its result type to convert it to St nat.

Instead, if you let-bind the effectful subterm, you're left with op_Multiply x x : Tot int, which we can easily subsume to Tot nat, then lift to St nat etc.

This patch is relatively easy, but clearly sub-optimal in terms of convenience. Hope to add variance annotations to the parameters of our inductive types and to improve this (#65)