Unable to prove post condition without explicit assertion

[jaybosamiya]

For the code that follows: F is unable to prove the last function (i.e. createSingletonList, unless I explicitly pass in any of the 3 commented out asserts; but when I uncomment any of them, F is able to prove it).

Also, since you asked, tagging: @nikswamy @aseemr @mtzguido

module DListTestCase

open FStar
open FStar.Ghost
open FStar.Seq
open FStar.HyperStack
open FStar.HyperStack.ST
open FStar.Buffer
open FStar.Int
open C
open C.Nullity
module U64 = FStar.UInt64
module U32 = FStar.UInt32
module U16 = FStar.UInt16
module U8 = FStar.UInt8
module Seq = FStar.Seq
module Ghost = FStar.Ghost
module ST = FStar.HyperStack.ST

unopteq
(** A doubly-linked list of a type*)
type dlist (t:Type0) = {
(* Forward link *)
  flink: pointer_or_null (dlist t);
(* Backward link *)
  blink: pointer_or_null (dlist t);
(* payload *)
  p: t;
}

unopteq
(** Head of a doubly linked list *)
type dlisthead (t:Type) = {
  (* head forward link *)
  lhead: pointer_or_null (dlist t);
  (* head backward link *)
  ltail: pointer_or_null (dlist t);
  (* all nodes in this dlist *)
  nodes: erased (seq (dlist t))
}

(** Be able to use [null] very very easily *)
inline_for_extraction private unfold
let null #t = null t

(** Initialze an element of a doubly linked list *)
let empty_entry (#t:Type) (payload:t): dlist(t) =
  { flink = null; blink = null; p = payload; }

(** Initialize a doubly-linked list head *)
let empty_list (#t:Type) : dlisthead t =
  { lhead = null; ltail = null; nodes = hide createEmpty}

unfold let op_At_Bang (#t:Type) (h0:mem) (p:pointer t) = Buffer.get h0 p 0
unfold let op_String_Access = Seq.index
unfold let not_null (#t:Type) (a:pointer_or_null t) = Buffer.length a <> 0

let _ = assert_norm (forall (t:Type) (p:pointer_or_null t). is_null p \/ not_null p)

unfold
let dlist_is_valid (#t:Type) (d:dlist t) =
  disjoint_1 d.flink d.blink

let _ = assert_norm (forall t p. dlist_is_valid (empty_entry #t p))

let dlisthead_nullness (#t:Type) (h0:mem) (h:dlisthead t) =
  let nodes = Ghost.reveal h.nodes in
  let l : nat = Seq.length nodes in
  (l > 0 ==> (not_null h.ltail /\ not_null h.lhead /\
              is_null (h0@! h.lhead).blink /\
              is_null (h0@! h.ltail).flink)) /\
  (l = 0 ==> (is_null h.ltail /\ is_null h.lhead))

let dlisthead_liveness (#t:Type) (h0:mem) (h:dlisthead t) =
  let nodes = Ghost.reveal h.nodes in
  let l = Seq.length nodes in
    live h0 h.lhead /\ live h0 h.ltail

let non_empty_dlisthead_connect_to_nodes (#t:Type) (h0:mem) (h:dlisthead t) =
  let nodes = Ghost.reveal h.nodes in
  let l : nat = Seq.length nodes in
  dlisthead_nullness h0 h /\
  (l > 0 ==> (h0@! h.ltail == nodes.[l-1] /\
              h0@! h.lhead == nodes.[0]))

let non_empty_dlisthead_is_valid (#t:Type) (h0:mem) (h:dlisthead t) =
  let nodes = Ghost.reveal h.nodes in
  let l = Seq.length nodes in
  let nonempty = l > 0 in
  non_empty_dlisthead_connect_to_nodes h0 h /\
  True

let dlisthead_is_valid (#t:Type) (h0:mem) (h:dlisthead t) =
  dlisthead_liveness h0 h /\
  non_empty_dlisthead_is_valid h0 h

let _ = assert_norm (forall t h0. dlisthead_nullness #t h0 empty_list)

unfold
let dlist_is_member_of (#t:eqtype) (h0:mem) (e:pointer (dlist t)) (h:dlisthead t) =
  Seq.mem (h0@! e) (Ghost.reveal h.nodes)

unfold
let erased_single_node (#t:eqtype) (e:pointer (dlist t)) =
  hide (Seq.create 1 !*e)

let foobar (#t:eqtype) (h1:mem) (y:dlisthead t) (h2:mem) =
  dlisthead_liveness h1 y /\ dlisthead_is_valid h2 y

let createSingletonList (#t:eqtype) (e:pointer (dlist t)): StackInline (dlisthead t)
    (requires (fun h0 -> live h0 e))
    (ensures (fun h1 y h2 -> modifies_1 e h1 h2 /\ live h2 e /\ foobar h1 y h2)) =
  let h1 = ST.get () in
  e.(0ul) <- { !*e with flink=null; blink = null };
  let y = { lhead = e; ltail = e; nodes = erased_single_node e } in
  assert (Seq.length (Ghost.reveal y.nodes) == 1);
  let h2 = ST.get () in
  // assert (foobar h1 y h2);
  // assert (equal_stack_domains h1 h2);
  // assert (dlisthead_is_valid h2 y);
  y

[nikswamy]

Hi Jay,

Here (below) is a version of the program that works without trouble or additional assertions.

The main diff is related to the three top-level assertion terms. These are encoded to the SMT solver as is, effectively introducing 3 unguarded quantifiers to the solver, which then sends its search off the rails.

Search below for "//HERE".

I've shown three alternative ways of writing test assertions of the form let _ = assert (forall t p . Phi).

1. Write it as let test () = assert (forall t p. Phi). This will check the assertion and then encode test () to the solver, but unless there is an application of test in your program somewhere, this encoding is benign.

2. Alternatively, you could write let test t p = assert Phi which is essentially equivalent.

3. If you really want to retain your original style, then I recommend tagging it with the opaque_to_smt attribute so that you don't end up polluting the solver's context.

[@opaque_to_smt]
let _ = assert (forall t p. Phi)

Also, you've been writing assert_norm instead of assert. This is fine, but quite unusual ... unless you really expect a lot of the proof to be done by simply computing in F*'s normalizer, I would suggest sticking to plain old assert.

Hope this helps ... closing for now. Please re-open is similar troubles persist. Nik,

@parno @protz you guys may be interested in this reply too.

module DListTestCase

open FStar
open FStar.Ghost
open FStar.Seq
open FStar.HyperStack
open FStar.HyperStack.ST
open FStar.Buffer
open FStar.Int
open C
open C.Nullity
module U64 = FStar.UInt64
module U32 = FStar.UInt32
module U16 = FStar.UInt16
module U8 = FStar.UInt8
module Seq = FStar.Seq
module Ghost = FStar.Ghost
module ST = FStar.HyperStack.ST

unopteq
(** A doubly-linked list of a type*)
type dlist (t:Type0) = {
(* Forward link *)
  flink: pointer_or_null (dlist t);
(* Backward link *)
  blink: pointer_or_null (dlist t);
(* payload *)
  p: t;
}

unopteq
(** Head of a doubly linked list *)
type dlisthead (t:Type) = {
  (* head forward link *)
  lhead: pointer_or_null (dlist t);
  (* head backward link *)
  ltail: pointer_or_null (dlist t);
  (* all nodes in this dlist *)
  nodes: erased (seq (dlist t))
}

(** Be able to use [null] very very easily *)
inline_for_extraction private unfold
let null #t = null t

(** Initialze an element of a doubly linked list *)
let empty_entry (#t:Type) (payload:t): dlist(t) =
  { flink = null; blink = null; p = payload; }

(** Initialize a doubly-linked list head *)
let empty_list (#t:Type) : dlisthead t =
  { lhead = null; ltail = null; nodes = hide createEmpty}

unfold let op_At_Bang (#t:Type) (h0:mem) (p:pointer t) = Buffer.get h0 p 0
unfold let op_String_Access = Seq.index
unfold let not_null (#t:Type) (a:pointer_or_null t) = Buffer.length a <> 0

//HERE
let test0 () = assert_norm (forall (t:Type) (p:pointer_or_null t). is_null p \/ not_null p)

unfold
let dlist_is_valid (#t:Type) (d:dlist t) =
  disjoint_1 d.flink d.blink

//HERE
let test1 t p = assert_norm (dlist_is_valid (empty_entry #t p))

let dlisthead_nullness (#t:Type) (h0:mem) (h:dlisthead t) =
  let nodes = Ghost.reveal h.nodes in
  let l : nat = Seq.length nodes in
  (l > 0 ==> (not_null h.ltail /\ not_null h.lhead /\
              is_null (h0@! h.lhead).blink /\
              is_null (h0@! h.ltail).flink)) /\
  (l = 0 ==> (is_null h.ltail /\ is_null h.lhead))

let dlisthead_liveness (#t:Type) (h0:mem) (h:dlisthead t) =
  let nodes = Ghost.reveal h.nodes in
  let l = Seq.length nodes in
    live h0 h.lhead /\ live h0 h.ltail

let non_empty_dlisthead_connect_to_nodes (#t:Type) (h0:mem) (h:dlisthead t) =
  let nodes = Ghost.reveal h.nodes in
  let l : nat = Seq.length nodes in
  dlisthead_nullness h0 h /\
  (l > 0 ==> (h0@! h.ltail == nodes.[l-1] /\
              h0@! h.lhead == nodes.[0]))

let non_empty_dlisthead_is_valid (#t:Type) (h0:mem) (h:dlisthead t) =
  let nodes = Ghost.reveal h.nodes in
  let l = Seq.length nodes in
  let nonempty = l > 0 in
  non_empty_dlisthead_connect_to_nodes h0 h /\
  True

let dlisthead_is_valid (#t:Type) (h0:mem) (h:dlisthead t) =
  dlisthead_liveness h0 h /\
  non_empty_dlisthead_is_valid h0 h

//HERE
[@"opaque_to_smt"]
let test = assert (forall t h0. dlisthead_nullness #t h0 empty_list)

unfold
let dlist_is_member_of (#t:eqtype) (h0:mem) (e:pointer (dlist t)) (h:dlisthead t) =
  Seq.mem (h0@! e) (Ghost.reveal h.nodes)

unfold
let erased_single_node (#t:eqtype) (e:pointer (dlist t)) =
  hide (Seq.create 1 !*e)

let foobar (#t:eqtype) (h1:mem) (y:dlisthead t) (h2:mem) =
  dlisthead_liveness h1 y /\ dlisthead_is_valid h2 y

let createSingletonList (#t:eqtype) (e:pointer (dlist t)): StackInline (dlisthead t)
    (requires (fun h0 -> live h0 e))
    (ensures (fun h1 y h2 -> modifies_1 e h1 h2 /\ live h2 e /\ foobar h1 y h2)) =
  let h1 = ST.get () in
  e.(0ul) <- { !*e with flink=null; blink = null };
  let y = { lhead = e; ltail = e; nodes = erased_single_node e } in
  //  assert (Seq.length (Ghost.reveal y.nodes) == 1);
  let h2 = ST.get () in
  // assert (foobar h1 y h2);
  // assert (equal_stack_domains h1 h2);
  // assert (dlisthead_is_valid h2 y);
  y

[jaybosamiya]

Ah, this makes sense. I was unaware that placing let _ = assert (something) at the top level would be this harmful to the solver.

Just as a clarification: as I understood it (earlier at least), any asserts inside a let binding would only be useful inside the binding, and would not escape it (for example, if we said let foo = assert(bar); (), then foo would just be a unit and the bar would not escape; and that let _ = assert(bar) would just be an easier way to say it). Is this something that is held to be true? (clearly, the example shows that my understanding of this was wrong; but I am not yet certain as to which part of my reasoning about the escaping is wrong) Or is it that the quantifiers cause it to behave differently than this?

I will be using three alternative ways you have suggested henceforth, but would love some clarification on the above question(s) as well.

Thanks a lot :)

[parno]

Discussed this with @nikswamy. The key difference is between let foo = and let foo() =; the latter won't leak into the context, unless you explicitly invoke foo, whereas the former will leak.

[jaybosamiya]

Ah, sounds good. Thanks :)

[jaybosamiya]

Discussed further with @parno and ran a bunch of tests. It seems confusing as to when stuff might or might not leak to the context.

The first set of tests:

let x0 = assume False
let y0 = assert (0 > 1)

let x1 () = assume False
let y1 = x1 (); assert (0 > 1)

let x2 () = assume False; assert (0 > 1)
let y2 = x2 (); assert (0 > 1)

let x3 () : Lemma (0 > 1) = assume False
let y3 = x3 (); assert (0 > 1) // This works

let x4 : Lemma (0 > 1) = assume False // "Effect Lemma used at unexpected position"

let x5 = assume False
let y5 = x5; assert (0 > 1)

Except for the *3 group, each of the rest fail. The *0 group shows that (at least) assume False does not leak directly. The *1 group confirms that assume False doesn't leak by explicitly calling the function it is defined in. The *2 group confirms that simply calling a function which has an assertion doesn't propagate that function. The *3 group works as expected. The *4 group demonstrates that one cannot leak a Lemma directly into the file (i.e. without an SMTPat or something similar). The *5 group is similar to *0 but shows that even invoking it doesn't cause it to leak.

2nd set of tests (testing quantifiers and triggers):

let _ = assume False; assert (forall x. {:pattern (id x)} id x > id (x + 1))
let _ = assert (id 0 > id (0 + 1))

It is unable to prove this, implying that the first assert did not leak here.

3rd set of tests (testing via trigger explosion):

assume val f : int -> int
let test = assume (forall x. {:pattern (f x)} f (f x) > f (x - 1))
let _ = assert (f (f 1) > f 0)

Here, we try to trigger an explosion in the context via a carefully chosen pattern. This doesn't seem to occur. Neither is it able to prove the assertion.

4th set of tests (trying various pattern/non-pattern combinations for quantifiers):

let _ = assume False; assert (forall i. {:pattern i} i > i + 1)
let _ = assume False; assert (forall i. i > i + 1)
let _ = assume False; assert (forall i. {:pattern (i > i + 1)} i > i + 1)
let _ = assert (0 > 0 + 1)
let _ = assert (forall i. i > i + 1)

It is unable to prove the final 2 lines.

---

Basically, it seems to me that the leaking behavior might not be as clear cut. It would be great @nikswamy if you could provide some insight into this.

Also, just from a language design perspective, I would assume that not leaking outside of a let binding should be expected behavior. I might be mistaken in understanding why this might be different from the code in the first post however, and it would be great if you could clarify if this is the case.

Thanks a lot :)

[aseemr]

Hi Jay, a couple of quick points (I could take a detailed look later):

-- The "leak" that @nikswamy mentioned means an unguarded assertion in the context of Z3 (or that's how I understand it). A top level assert with no arguments such as let x0 = assert phi is encoded to Z3 without any pattern, and that could send Z3 off the rails. Whereas, when we add some arguments, e.g. let x0 () = ..., the assertion is encoded with a pattern that controls the triggering behavior of this assertion (may be we can add a pattern in the no arguments case also, need to see more).

-- Regarding the behavior of let x0 = assume False and calling it from other functions: the reasoning of assert and assume happens via their type (see prims.fst, where you can see that the assumed or asserted formula becomes part of the type). The type of x0 itself however is simply Tot unit or Tot Type0, which does not provide the formula in the logical context when called from other functions. If instead you wrote let x0 () :Pure unit (requires True) (ensures (fun _ -> False)) = assume False, then calling x0 () from other functions would give you the behavior you expect. This is equivalent to what you wrote in *3 above, and even in that case, it is not assume False that is helping, but 0 > 1 which is part of the type (though they are the same morally).

Hope this helps, please add comments if you have more questions.

[nikswamy]

I still need to read in detail and comment. But, you may also be interested in #1208

[nikswamy]

Hi Jay, all.

Took me a while to get around to responding on this, sorry.

The explanation is a bit convoluted as there are two issues tangled together. So, please bear with me as I try to explain.

First: The logical content of Prims.assert, assert_norm, assume, admit, etc. at the top-level do not escape implicitly into the types of the let-bound names. So let x = assume False just has type unit rather than u:unit{False}---were it to have the latter type, then this would indeed pollute the context. But, this is actually because functions in Prims receive rather special handling in the SMTEncoding.

If you instead wrote this program, which is essentially equivalent, except you've rolled your own version of assume, then the assertion for y0 goes through.

assume val my_assume : p:Type0 -> Pure unit (requires True) (ensures (fun _ -> p))
let bad= my_assume False
let y0 = assert (0 > 1)

So, what's going on here:

1. The definitions of pure or ghost top-level terms are made available in the logical context. For instance, if you wrote let x : list nat = [0; 1; 2] then an encoding of the list term [0;1;2] is bound to x in the SMT context, together with a typing assumption that x has type (encoding of) list nat. Even this will introduce some overhead into your context. Notably, there are axioms available at the top-level which allows inverting typing assumptions on inductive types. This will trigger a few times (up to the ifuel limit) on [0;1;2] producing formulae such as HasType 0 nat, HasType [1;2] (list nat) ,HasType 1 nat,HasType [2] (list nat)` etc.

For a term f at a function type x:t -> Pure t' pre post (the same also applies for Ghost ), an axiom states roughly that forall x. HasType x t /\ pre ==> HasType (f x) t' /\ post (HasType f x). So, in my example, the definition of bad is given at the top-level as my_assume False and the typing axiom for my_assume gives us that HasType False Type0 ==> False, which is enough to render the context inconsistent.

It turns out that special handling of pure functions in Prims meant that this typing axiom for Prims._assume was not present. So, in your program:

let x0 = assume False
let y0 = assert (0 > 1)

x0 is encoded to the top-level as Prims._assume False and then nothing further happens, since the specially-handled type of Prims._assume doens't allow the SMT solver to conclude anything further.

2. Now, in your original example, what you had was something like

let x0 = assert (forall x. Phi)

Again, this definition was encoded to the SMT solver as Prims._assert Q where Q is the encoding of forall x. Phi. This time, even though the type of Prims._assert is benign, the mere presence of the term Q in the the SMT context, allowed the forall-interp axiom to trigger (more about that axiom in #1208 and #1059), which sent your proof off the rails.

---

Now, what to do about all this:

1. I am trying a patch (that I've described before in #1059) where the SMT encoding encodes terms that are ascribed the unit type as the constant Tm_unit. This should help prevent needless yet problematic terms like the term encoding of quantified formulas to the SMT solver in most common cases. With this patch, I expect your original program to work as you wrote it.

Note, this patch caused 1 regression in the benchmark suite on an example which I think was rather brittle to begin with in any case: @mtzguido you might be interested to see the change in NormVsSmt: aa94aad99e3ec4fe330b150a0784ca0a1357a040

2. That said, be careful when introducing top-level definitions. Even simple things like [0;1;2] can introduce some (usually small) solver overhead. Note especially that the patch described point (1) above only applies to unit-typed terms. So, you can still shoot yourself in the foot by doing things like:

assume val my_assume_bool : p:Type0 -> Pure bool (requires True) (ensures (fun _ -> p))
let bad= my_assume_bool False
let y0 = assert (0 > 1)

[nikswamy]

OH, and thanks for the analysis and bringing this mess to light.

[jaybosamiya]

First off, thanks a lot @aseemr and @nikswamy. It definitely did clarify it up a lot.

Just a few minor lingering questions:

The logical content of Prims.assert, assert_norm, assume, admit, etc. at the top-level do not escape implicitly into the types of the let-bound names.

As far as I understand (from a few tests I ran), they do seem to escape even on non-top-level lets (i.e., in a let inside a let; for eg: let x = let y = assume False in assert (0 > 1)). If we didn't want it to escape there, is there a nice way? Basically, I am thinking about this from a "structuring the proof" perspective, where I might want to prove sublemmas within the proof of the lemma itself, but not create a top-level lemma for it.

the mere presence of the term Q in the the SMT context, allowed the forall-interp axiom to trigger

I am not entirely sure I understand this. I will try reading more about this to try to understand it and will ask a more concrete question once I am actually sure about what I don't understand about it :)

Thanks again! :)

[nikswamy]

In a term like this;

let x = let y = assume False in assert (0 > 1)).

the assume is most definitely intended to be in scope in the continuation. This is just an instance of a post-condition of one computation being available in its continuation.

Top-level definitions are exempt from this behavior (at least we aim for them to be, modulo the behaviors/bugs discussed on this thread) in that the post-condition of a top-level computation is not sequenced with specifications of effectful top-level terms that follow it. Indeed, top-level effects are not fully supported by F*, although this document describes where we hope to go with that: https://github.com/FStarLang/FStar/wiki/Top-level-effects

As for hiding logical information in the local context, something like this should work:

assume val only_this_formula : Type0
let f = 
   let expose () : Lemma only_this_formula = 
        assume False
   in
  expose ();
  assert only_this_formula; //works
  assert False //should fail

[nikswamy]

Is there anything remaining to be addressed here? If not, I'd like to close it.

[jaybosamiya]

Thanks a lot :) Closing this.