Require stage in induction hypothesis

[EmilyOng]

Contradictory program returns true for entailment:

let rec all_threes xs =
  match xs with
  | [] -> true
  | x :: xs' -> x = 3 && all_threes xs'

let foo xs
(* Note: Here, we use structural equality =. The program works correctly if we use -> *)
(*@ req xs=[1]; ens res=true @*)
= all_threes xs

========== Function: foo ==========
[Specification] req xs=1::[]; ens res=true

[Normed   Spec] req xs=1::[]; ens res=true

[Raw Post Spec] ens emp; ex v35; all_threes(xs, v35); ens res=v35

[Normed   Post] ex v35; all_threes(xs, v35); ens res=v35

[Forward  Time] 10 ms
[Entail  Check] true
[Entail   Time] 221 ms
[Z3       Time] 317 ms
===================================

The problem appears to be here, in the application of the induction hypothesis, where the "require" specification get carried over in the unfolding. This IH also seems unexpected.

==== apply IH | _2648 ====
IH: forall [xs; res], all_threes(xs,res) <: req xs=1::[]; ens res=true

after:
ex v55 v56 v57 v58; ens xs=v57::v58/\v56=(v57==3)/\T; req v58=1::[]; ens v55=true; ex v35; ens res=v56 && v55
<:
req xs=1::[]; ens res=true

Note: This is why I thought the test1/2/3 programs in all.ml were working.

We can try to workaround it like so:

let rec all_threes xs =
  match xs with
  | [] -> true
  | x :: xs' -> x = 3 && all_threes xs'

let goo xs
(* Entailment fails. *)
(*@ ens res=true @*)
= all_threes xs

let foo xs
(* Put the specification on the caller only *)
(*@ req xs=[1] @*)
= goo xs