Restricting well-foundedness on inductives function-typed fields

[nikswamy]

This is related to #2205

The PR 2205 says: "this fix enhances the SMT encoding of inductives to include an additional property on f x << D f for data constructors D of an inductive t whose argument include a ghost or total function returning a t"

However, the PR was actually introducing this axiom for all ghost or total function-typed fields, not just those returning an element of the (mutual) inductive t.

This allows the following unsoundness (shown below), which @Chris-Hawblitzel found yesterday ... thanks Chris! Effectively, this example replays the older unsoundness described in #2069 using a boxed dependent function (my_fun_dep). This patch blocks this kind of example.

This PR actually restricts the axiom to function-typed fields returning one of the (mutual) inductives. I've added Chris' example to tests/micro-benchmarks/TestWellFoundedRecursion.fst and lemma_my_fun_dep and lemma_my_fun are no longer provable.

Note, this also means that examples like this are no longer provable, since we do not generate any well-foundedness axiom for Test1.f.

noeq
type test1 (a:Type) =
  | Test1: f:(nat -> a) -> test1 a

noeq
type test2 (a:Type) =
  | Test2: g:test1 (test2 a) -> test2 a

let wf_test1 (#a:_) (x:test1 a) (y:nat)
  : Lemma (Test1?.f x y << x)
  = ()

But, that this example worked was perhaps just a quirk, since similar examples also were never supported:

noeq
type stream' (a:Type) =
  | SNil': stream' a
  | SCons': a & (unit -> stream' a) -> stream' a

where the function in the second component of the pair in SCons' does not get a well-foundedness axiom.

I have an F* and Everest green with this patch.

Looking beyond this PR: The root cause of this class of issues is that F*'s encoding to SMT erases the universe annotations. Retaining universes in the SMT encoding is the right thing to do and I plan to revive the work in nik_smt_univs towards that end.

noeq
type my_fun_dep (a: Type) (b: a -> Type) =
  | MyFunDep : (y: a -> b y) -> my_fun_dep a b

type my_fun (a: Type u#n) (b: Type u#m) = my_fun_dep a (fun _ -> b)

let app_dep (#a: Type) (#b: a -> Type) (f: my_fun_dep a b) (x: a) 
  : b x
  = let MyFunDep f_inner = f in
    f_inner x

let app (#a: Type u#n) (#b: Type u#m) (f: my_fun a b) (x: a) : b =
  let MyFunDep f_inner = f in
  f_inner x

let lemma_my_fun_dep (#a: Type) (#b: (a -> Type)) (f: my_fun_dep a b) (x: a)
  : Lemma (app_dep f x << f)
  = ()

let lemma_my_fun (#a: Type u#n) (#b: Type u#m) (f: my_fun a b) (x: a)
  : Lemma (app f x << f)
  = ()

let id
  : my_fun_dep (Type u#m) (fun (a : Type u#m) -> my_fun a a)
  = MyFunDep (fun (a : Type u#m) -> MyFunDep (fun (x : a) -> x))

let lem ()
  : Lemma (id << id)
  = let t : Type u#1 = my_fun_dep (Type u#0) (fun (a:Type u#0) -> my_fun a a) in
    lemma_my_fun (app_dep (id u#1) t) (id u#0);
    lemma_my_fun_dep #(Type u#1) #(fun a -> my_fun a a) (id u#1) t;
    assert (id u#0 << id u#1);
    ()

let falso2 ()
  : Lemma False
  = lem ()

[mtzguido]

Looks good to me. Maybe we can add this test in the same file, as a reminder:

noeq
type ind = | Mk : (int -> ind u#0) -> ind u#aa

which has to (and does) fail due to the variance in universe levels for ind.

[TWal]

FYI, this breaks one of my former developments:

open FStar.List.Pure
open FStar.FunctionalExtensionality
open FStar.Bytes

noeq type comb (n:nat) (ret_type:Type) =
  | Comb: send: FStar.Bytes.bytes -> cont:((llist FStar.Bytes.bytes n) -> ret_type){is_restricted (llist FStar.Bytes.bytes n) cont} -> comb n ret_type

#push-options "--ifuel 1"
val fmap_comb_flip: #n:nat -> #b:Type -> #c:Type -> x:comb n b -> f:(y:b{y<<x} -> c) -> comb n c
let fmap_comb_flip #n x f =
  let Comb xa fb = x in
  let cont vb =
    f (fb vb)
  in
  Comb xa (FStar.FunctionalExtensionality.on _ cont)
#pop-options

val fmap_comb: #n:nat  -> #b:Type -> #c:Type -> (b -> c) -> comb n b -> comb n c
let fmap_comb #n f x =
  fmap_comb_flip x f

noeq type comba (n:nat) (ret:Type) =
  | Abort: comba n ret
  | Ret: v:ret -> comba n ret
  | Com: v:comb n (comba n ret) -> comba n ret

#push-options "--ifuel 1"
val join_comba: #n:nat -> #ret:Type -> comba n (comba n ret) -> comba n ret
let rec join_comba #n #ret x =
  match x with
  | Abort -> Abort
  | Ret r -> r
  | Com y ->
    Com (fmap_comb_flip y join_comba)
#pop-options

I guess the solution would be to inline comb inside comba, but the change is non-trivial and it's not clear how it impacts the rest of the development.

[nikswamy]

Thanks for the comment @TWal. Is it possible for you to evaluate the impact?

[nikswamy]

@TWal : I added an option --ext 'compat:2954' to not break your code.

open FStar.List.Pure
open FStar.FunctionalExtensionality
open FStar.Bytes

#push-options "--ext 'compat:2954'"
noeq type comb (n:ℕ) (ret_type:Type) =
  | Comb: send: FStar.Bytes.bytes → cont:((llist FStar.Bytes.bytes n) → ret_type){is_restricted (llist FStar.Bytes.bytes n) cont} → comb n ret_type
#pop-options

#push-options "--ifuel 1"
val fmap_comb_flip: #n:ℕ → #b:Type → #c:Type → x:comb n b → f:(y:b{y≪x} → c) → comb n c
let fmap_comb_flip #n x f =
  let Comb xa fb = x in
  let cont vb =
    f (fb vb)
  in
  Comb xa (FStar.FunctionalExtensionality.on _ cont)
#pop-options

val fmap_comb: #n:ℕ  → #b:Type → #c:Type → (b → c) → comb n b → comb n c
let fmap_comb #n f x =
  fmap_comb_flip x f

noeq type comba (n:ℕ) (ret:Type) =
  | Abort: comba n ret
  | Ret: v:ret → comba n ret
  | Com: v:comb n (comba n ret) → comba n ret

#push-options "--ifuel 1"
val join_comba: #n:ℕ → #ret:Type → comba n (comba n ret) → comba n ret
let rec join_comba #n #ret x =
  match x with
  | Abort → Abort
  | Ret r → r
  | Com y →
    Com (fmap_comb_flip y join_comba)
#pop-options

With this, your code works, while raising the warning:

(Warning 337) Using 'compat:2954' to use a permissive encoding of the subterm ordering on the codomain of a constructor.
This is deprecated and will be removed in a future version of F*.