Open nikswamy opened 3 years ago
Some progress on this, PR #2227 addresses issue 3, fixing errors in the unifier. Still investigating the SMT failures.
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
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 https://github.com/FStarLang/FStar/issues/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
Some examples ... all the expect failures shouldn't really fail, but they currently do.
This works:
But, this doesn't:
Doesn't really seem related to atomic, since this also fails: