Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

SMTEncoding of impure arrows comes in the way of verification #855

Open
aseemr opened this issue Feb 13, 2017 · 3 comments

Comments

@aseemr
Copy link
Contributor

@aseemr aseemr commented Feb 13, 2017

The following example does not verify:

val bar: unit -> St (unit -> St nat)
let bar () =
  let r = alloc 2 in
  let f:(unit -> St nat) = fun () -> !r in
  f

On debugging, I found that the problem is because F* encodes the arrow type unit -> St nat (at least) twice, and is not able to reason that it's the same type.

So, I tried the following version, and it works:

type fn = unit -> St nat

val bar: unit -> St fn
let bar () =
  let r = alloc 2 in
  let f:fn = ((fun () -> !r) <: fn) in
  f

Perhaps the annotations cause unit -> St nat to be encoded just once.

We don't encode any HasType axiom for impure arrows, and so this problem comes (I suspect that for pure arrows the HasType enables some reasoning of two encodings of the same type). Can we make hashconsing smarter so that it does not encode same impure arrow twice (or perhaps it already is?).

@aseemr

This comment has been minimized.

Copy link
Contributor Author

@aseemr aseemr commented Feb 14, 2017

We could do two things here:

  1. Make hash consing of arrow types more precise, so that it takes into account the effect label, the return type, and the wp.

  2. Add HasType axiom for total effectful arrows (along the lines of what we do for pure arrows).

(1) is anyway good to have for working with Div code.

@kyoDralliam

This comment has been minimized.

Copy link
Contributor

@kyoDralliam kyoDralliam commented Nov 12, 2017

One strange observation (at least to me), the following code does not need as much typing annotations nor let-bindings (maybe because it is done automatically in the typechecker)

val bar2: unit -> St (fn * unit)
let bar2 () =
  let r : ref nat = alloc 2 in
  (fun () -> !r), ()
@shravanrn

This comment has been minimized.

Copy link

@shravanrn shravanrn commented Mar 17, 2019

Was requested by assem to post the following example here, which may be another instance of this issue

Below, I am trying to ensure that e and h always have the same length.

module DepStruct

module HST = FStar.HyperStack.ST
module I32 = FStar.Int32
module Seq = FStar.Seq

noeq
type wf_Q = 
  | Q_Cons :
    e : Seq.seq int ->
    h : (me:Seq.seq (int -> int -> HST.St int){ Seq.length e = Seq.length me}) ->
  wf_Q

let main() : HST.St I32.t =
  let q : wf_Q = Q_Cons Seq.empty Seq.empty in
  0l

But the program gives the following type error

DepStruct.fst(11,4-11,12): (Error 19) Subtyping check failed; expected type me:
FStar.Seq.Base.seq (_: Prims.int -> _: Prims.int -> FStar.HyperStack.ST.St Prims.int)
  {FStar.Seq.Base.length (Q_Cons?.events projectee) = FStar.Seq.Base.length me}; got type me:
FStar.Seq.Base.seq (_: Prims.int -> _: Prims.int -> FStar.HyperStack.ST.St Prims.int)
  {FStar.Seq.Base.length events = FStar.Seq.Base.length me} (see also DepStruct.fst(11,55-11,88))
DepStruct.fst(15,34-15,43): (Error 19) Subtyping check failed; expected type me:
FStar.Seq.Base.seq (_: Prims.int -> _: Prims.int -> FStar.HyperStack.ST.St Prims.int)
  {FStar.Seq.Base.length FStar.Seq.Base.empty = FStar.Seq.Base.length me}; got type s:
FStar.Seq.Base.seq (_: Prims.int -> _: Prims.int -> FStar.HyperStack.ST.St Prims.int)
  {FStar.Seq.Base.length s = 0} (see also DepStruct.fst(11,55-11,88))
Verified module: DepStruct (1225 milliseconds)
2 errors were reported (see above)

This does work when i change the effect from St to Pure

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
4 participants
You can’t perform that action at this time.