Difficulties with refinement subtyping in Steel

[nikswamy]

Some examples ... all the expect failures shouldn't really fail, but they currently do.

1. Moving a refinement into the ensures clause seems to require an explicit let binding

assume
val test (_:unit) :
  SteelT nat emp (fun _ -> emp)

[@@expect_failure]
let use (_:unit) :
  Steel int emp (fun _ -> emp)
        (requires fun _ -> True)
        (ensures fun _ x _ -> (x >= 0) == true)
  = test() //SMT failure

let shift (_:unit) :
  Steel int emp (fun _ -> emp)
        (requires fun _ -> True)
        (ensures fun _ x _ -> (x >= 0) == true)
  = let x = test() in x

2. We seem to need to promote SteelAtomic to SteelT before using it as Steel

module SEA= Steel.Effect.Atomic

assume
val atomic (#uses:_) (p:prop)
  : SEA.SteelAtomic (u:unit{p}) uses SEA.unobservable emp (fun _ -> emp)

let use_atomic (p:prop)
  : SteelT (u:unit{p})  emp (fun _ -> emp)
  = atomic p

[@@expect_failure]
let use_atomic_shift (p:prop)
  : Steel unit emp (fun _ -> emp) (fun _ -> True) (fun _ _ _ -> p)
  = atomic p

[@@expect_failure]
let use_atomic_shift (p:prop)
  : Steel unit emp (fun _ -> emp) (fun _ -> True) (fun _ _ _ -> p)
  = let _ = atomic p in ()

[@@expect_failure]
let use_atomic_shift (p:prop)
  : Steel unit emp (fun _ -> emp) (fun _ -> True) (fun _ _ _ -> p)
  = use_atomic p //SMT failure

let use_atomic_shift (p:prop)
  : Steel unit emp (fun _ -> emp) (fun _ -> True) (fun _ _ _ -> p)
  = let x = use_atomic p in x

3. Local let bindings

This works:

assume 
val f (_:unit) :
  SteelT unit emp (fun _ -> emp)

let g (_:unit)
  : SteelT unit emp (fun _ -> emp) = 
  let f2 () 
    : SteelT unit emp (fun _ -> emp)
    = f (); f ()
  in
  f2 ()

But, this doesn't:

let elim_pure (p:prop)
  : Steel unit (pure p) (fun _ -> emp)
   (requires fun _ -> True)
   (ensures fun _ _ _ -> p)
  = let elim_pure_alt (p:prop)
      : SteelT (_:unit{p}) (pure p) (fun _ -> emp)
      = let _ = Steel.Effect.Atomic.elim_pure p in ()
    in
    let x = elim_pure_alt p in
    ()

Doesn't really seem related to atomic, since this also fails:

assume
val f (p:prop) :
  SteelT (u:unit{p}) emp (fun _ -> emp)

let g (p:prop)
  : Steel unit emp (fun _ -> emp) (requires fun _ -> True) (ensures fun _ _ _ -> p) =
  let f2 (p:prop)
    : SteelT (u:unit{p}) emp (fun _ -> emp)
    = f p
  in
  let x = f2 p in x

[R1kM]

Some progress on this, PR FStarLang/FStar#2227 addresses issue 3, fixing errors in the unifier. Still investigating the SMT failures.

[R1kM]

Minimizing further 1. and 2. The third expect_failure of 2. is also already verifying

assume
val refined (p:prop)
  : SteelT (u:unit{p})  emp (fun _ -> emp)

let shift (p:prop)
  : Steel unit emp (fun _ -> emp) (fun _ -> True) (fun _ _ _ -> p)
  = refined p //SMT failure

[R1kM]

Minimizing further 2. by removing Steel-specific details. The following also fails

type repr (a:Type) (_:unit) = a
let return (a:Type) (x:a) : repr a () = x
let bind (a:Type) (b:Type) (f:repr a ()) (g:a -> repr b ()) : repr b () = g f
let subcomp (a:Type) (f:repr a ()) : repr a () = f

reifiable
layered_effect {
  M :(a:Type) -> (_:unit) -> Effect
  with repr = repr; return = return; bind = bind; subcomp = subcomp
}

unfold
let bind_pure_req (#a:Type) (wp:pure_wp a) = as_requires wp

assume
val bind_pure_m (a:Type) (b:Type)
  (wp:pure_wp a)
  (f:eqtype_as_type unit -> PURE a wp) (g:a -> repr b ())
 : Pure (repr b ()) (requires bind_pure_req wp) (ensures fun _ -> True)

polymonadic_bind (PURE, M) |> M = bind_pure_m

assume val refined (p:prop) : M (u:unit{p}) ()

let shift (p:prop) : M unit () = refined p

This seems to be related to FStarLang/FStar#881 . Steel needs to be defined as reifiable to implement par for two arbitrary Steel computations by lifting the definitional interpreter. Unfortunately, subtyping is not allowed for reifiable functions. This seems to be the same problem for 1.

As observed previously, a workaround is always to let-bind the problematic computation