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.

Sign up for GitHub

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

Jump to bottom

Unifier causing normalization loops (zeta enabled in equal heuristic) #3207

Open
andricicezar opened this issue Feb 8, 2024 · 4 comments
Open

Unifier causing normalization loops (zeta enabled in equal heuristic) #3207

andricicezar opened this issue Feb 8, 2024 · 4 comments

Comments

@andricicezar
Copy link

andricicezar commented Feb 8, 2024 •
edited

Hi, I have a use case when normalization loops.
image

Using F* version: 2024.01.13

Sorry for the big file. I removed as many things as I had time. The problem is with verifying the last definition:

(* Based on file FStar/examples/metatheory/StlcStrongDbParSubst.fst *)

module Bug

open FStar.Tactics
open FStar.Constructive
open FStar.Classical
open FStar.FunctionalExtensionality

(* Constructive-style progress and preservation proof for STLC with
   strong reduction, using deBruijn indices and parallel substitution. *)

type typ =
  | TArr    : typ -> typ -> typ
  | TSum    : typ -> typ -> typ
  | TPair   : typ -> typ -> typ
  | TUnit   : typ
  | TNat    : typ

type var = nat

open FStar.Bytes

type exp =
  | EVar         : var -> exp
  | EApp         : exp -> exp -> exp
  | ELam         : typ -> exp -> exp
  | EUnit        : exp
  | EZero        : exp
  | ESucc        : v:exp -> exp
  | ENRec        : exp -> exp -> exp -> exp
  | EInl         : v:exp -> exp
  | EInr         : v:exp -> exp
  | ECase        : exp -> exp -> exp -> exp
  | EFst         : exp -> exp
  | ESnd         : exp -> exp
  | EPair        : fst:exp -> snd:exp -> exp


(* Type system; as inductive relation (not strictly necessary for STLC) *)

type env = var -> Tot (option typ)

val empty : env
let empty _ = None

(* we only need extend at 0 *)
val extend : typ -> env -> Tot env
let extend t g y = if y = 0 then Some t
                   else g (y-1)

noeq type typing : env -> exp -> typ -> Type =
  | TyVar : #g:env ->
             x:var{Some? (g x)} ->
             typing g (EVar x) (Some?.v (g x))
  | TyLam : #g :env ->
             t :typ ->
            #e1:exp ->
            #t':typ ->
            $hbody:typing (extend t g) e1 t' ->
                   typing g (ELam t e1) (TArr t t')
  | TyApp : #g:env ->
            #e1:exp ->
            #e2:exp ->
            #t11:typ ->
            #t12:typ ->
            $h1:typing g e1 (TArr t11 t12) ->
            $h2:typing g e2 t11 ->
                typing g (EApp e1 e2) t12
  | TyUnit : #g:env ->
             typing g EUnit TUnit
  | TyZero : #g:env ->
             typing g EZero TNat
  | TySucc : #g:env ->
             #e:exp ->
             $h1:typing g e TNat ->
                 typing g (ESucc e) TNat
  | TyNRec : #g:env ->
             #e1:exp ->
             #e2:exp ->
             #e3:exp ->
             #t1:typ ->
             $h1:typing g e1 TNat ->
             $h2:typing g e2 t1 ->
             $h3:typing g e3 (TArr t1 t1) ->
                 typing g (ENRec e1 e2 e3) t1
  | TyInl  : #g:env ->
             #e:exp ->
             #t1:typ ->
             t2:typ ->
             $h1:typing g e t1 ->
                 typing g (EInl e) (TSum t1 t2)
  | TyInr  : #g:env ->
             #e:exp ->
             t1:typ ->
             #t2:typ ->
             $h1:typing g e t2 ->
                 typing g (EInr e) (TSum t1 t2)
  | TyCase : #g:env ->
             #e1:exp ->
             #e2:exp ->
             #e3:exp ->
             #t1:typ ->
             #t2:typ ->
             #t3:typ ->
             $h1:typing g e1 (TSum t1 t2) ->
             $h2:typing g e2 (TArr t1 t3) ->
             $h3:typing g e3 (TArr t2 t3) ->
                 typing g (ECase e1 e2 e3) t3
  | TyFst         : #g:env ->
                    #e:exp ->
                    #t1:typ ->
                    #t2:typ ->
                    $h1:typing g e (TPair t1 t2) ->
                        typing g (EFst e) t1
  | TySnd         : #g:env ->
                    #e:exp ->
                    #t1:typ ->
                    #t2:typ ->
                    $h1:typing g e (TPair t1 t2) ->
                        typing g (ESnd e) t2
  | TyPair        : #g:env ->
                    #e1:exp ->
                    #e2:exp ->
                    #t1:typ ->
                    #t2:typ ->
                    $h1:typing g e1 t1 ->
                    $h2:typing g e2 t2 ->
                        typing g (EPair e1 e2) (TPair t1 t2)

(* Parallel substitution operation `subst` *)
let sub (renaming:bool) = 
    f:(var -> exp){ renaming <==> (forall x. EVar? (f x)) }

let bool_order (b:bool) = if b then 0 else 1

let sub_inc 
  : sub true
  = fun y -> EVar (y+1)

let is_var (e:exp) : int = if EVar? e then 0 else 1

let rec subst (#r:bool)
              (s:sub r)
              (e:exp)
  : Tot (e':exp { r ==> (EVar? e <==> EVar? e') })
        (decreases %[bool_order (EVar? e); 
                     bool_order r;
                     1;
                     e])
  = match e with
  | EVar x -> s x
  | ELam t e1 -> ELam t (subst (sub_elam s) e1)
  | EApp e1 e2 -> EApp (subst s e1) (subst s e2)
  | EUnit -> EUnit
  | EZero -> EZero
  | ESucc e -> ESucc (subst s e)
  | ENRec e1 e2 e3 -> ENRec (subst s e1) (subst s e2) (subst s e3)
  | EInl e -> EInl (subst s e)
  | EInr e -> EInr (subst s e)
  | ECase e1 e2 e3 -> ECase (subst s e1) (subst s e2) (subst s e3)
  | EFst e -> EFst (subst s e)
  | ESnd e -> ESnd (subst s e)
  | EPair e1 e2 -> EPair (subst s e1) (subst s e2)

and sub_elam (#r:bool) (s:sub r) 
  : Tot (sub r)
        (decreases %[1;
                     bool_order r;
                     0;
                     EVar 0])
  = let f : var -> exp = 
      fun y ->
        if y=0
        then EVar y
        else subst sub_inc (s (y - 1))
    in
    introduce not r ==> (exists x. ~ (EVar? (f x)))
    with not_r. 
      eliminate exists y. ~ (EVar? (s y))
      returns (exists x. ~ (EVar? (f x)))
      with (not_evar_sy:squash (~(EVar? (s y)))). 
        introduce exists x. ~(EVar? (f x))
        with (y + 1)
        and ()
    ;
    f

let sub_beta (e:exp)
  : sub (EVar? e)
  = let f = 
      fun (y:var) ->
        if y = 0 then e      (* substitute *)
        else (EVar (y-1))    (* shift -1 *)
    in
    if not (EVar? e)
    then introduce exists (x:var). ~(EVar? (f x))
         with 0 and ();
    f

(* Small-step operational semantics; strong / full-beta reduction is
   non-deterministic, so necessarily as inductive relation *)

type step : exp -> exp -> Type =
  | SBeta : t:typ ->
            e1:exp ->
            e2:exp ->
            step (EApp (ELam t e1) e2) (subst (sub_beta e2) e1)
  | SApp1 : #e1:exp ->
             e2:exp ->
            #e1':exp ->
            $hst:step e1 e1' ->
                 step (EApp e1 e2) (EApp e1' e2)
  | SApp2 :   e1:exp ->
             #e2:exp ->
            #e2':exp ->
            $hst:step e2 e2' ->
                 step (EApp e1 e2) (EApp e1 e2')
  | SSucc :    e:exp ->
             #e':exp ->
            $hst:step e e' ->
                 step (ESucc e) (ESucc e')     
  | SNRecV :  #e1:exp ->
             #e1':exp ->
               e2:exp ->
               e3:exp ->
             $hst:step e1 e1' ->
                 step (ENRec e1 e2 e3) (ENRec e1' e2 e3)
  | SNRec0 : e2:exp ->
             e3:exp ->
                 step (ENRec EZero e2 e3) e2
  | SNRecIter :  v:exp ->
                e2:exp ->
                e3:exp ->
                step (ENRec (ESucc v) e2 e3) (ENRec v (EApp e3 e2) e3)
  | SInl  :    e:exp ->
             #e':exp ->
            $hst:step e e' ->
                 step (EInl e) (EInl e')
  | SInr  :    e:exp ->
             #e':exp ->
            $hst:step e e' ->
                 step (EInr e) (EInr e')
  | SCase :  #e1:exp ->
            #e1':exp ->
              e2:exp ->
              e3:exp ->
            $hst:step e1 e1' ->
                 step (ECase e1 e2 e3) (ECase e1' e2 e3)
  | SCaseInl :  v:exp ->
               e2:exp ->
               e3:exp ->
                 step (ECase (EInl v) e2 e3) (EApp e2 v)
  | SCaseInr :  v:exp ->
               e2:exp ->
               e3:exp ->
                 step (ECase (EInr v) e2 e3) (EApp e3 v)
  | SFst0 :    #e:exp ->
              #e':exp ->
             $hst:step e e' ->
                 step (EFst e) (EFst e')
  | SFst :  e1:exp ->
            e2:exp ->
               step (EFst (EPair e1 e2)) e1
  | SSnd0 :    #e:exp ->
              #e':exp ->
             $hst:step e e' ->
                 step (ESnd e) (ESnd e')
  | SSnd :  e1:exp ->
            e2:exp ->
               step (ESnd (EPair e1 e2)) e2
  | SPair1  : #e1:exp ->
             #e1':exp ->
             $hst:step e1 e1' ->
               e2:exp ->
                 step (EPair e1 e2) (EPair e1' e2)
  | SPair2  :  e1:exp ->
              #e2:exp ->
             #e2':exp ->
             $hst:step e2 e2' ->
                 step (EPair e1 e2) (EPair e1 e2')


let rec is_value (e:exp) : bool = 
     ELam? e || 
     EUnit? e || 
     EZero? e || 
     (ESucc? e && is_value (ESucc?.v e)) || 
     (EInl? e && is_value (EInl?.v e)) ||
     (EInr? e && is_value (EInr?.v e)) || 
     (EPair? e && is_value (EPair?.fst e) && is_value (EPair?.snd e) )

let rec progress (#e:exp { ~(is_value e) })
                 (#t:typ)
                 (h:typing empty e t)
  : e':exp & step e e'
  =  match h with
     | TyApp #g #e1 #e2 #t11 #t12 h1 h2 -> 
     begin
          match e1 with
          | ELam t e1' -> (| subst (sub_beta e2) e1', SBeta t e1' e2 |)
          | _          -> let (| e1', h1' |) = progress h1 in
                              (| EApp e1' e2, SApp1 e2 h1'|) (** TODO: call-by-name **)
     end
     | TySucc #g #e h1 ->
          let (| e', h1' |) = progress h1 in
          (| ESucc e', SSucc e h1'|)
     | TyNRec #g #e1 #e2 #e3 #t1 h1 h2 h3 -> begin
          match e1 with
          | EZero -> (| e2, SNRec0 e2 e3 |)
          | ESucc v -> (| ENRec v (EApp e3 e2) e3, SNRecIter v e2 e3 |)
          | _ -> let (| e1', h1' |) = progress h1 in
                 (| ENRec e1' e2 e3, SNRecV e2 e3 h1' |)
     end
     | TyInl #g #e #t1 #t2 h1 -> 
          let (| e', h1' |) = progress h1 in
          (| EInl e', SInl e h1'|)
     | TyInr #g #e #t1 #t2 h1 -> 
          let (| e', h1' |) = progress h1 in
          (| EInr e', SInr e h1'|)
     | TyCase #g #e1 #e2 #e3 #t1 #t2 #t3 h1 h2 h3 -> begin
          match e1 with
          | EInl v -> (| EApp e2 v, SCaseInl v e2 e3 |)
          | EInr v -> (| EApp e3 v, SCaseInr v e2 e3 |)
          | _ ->
               let (| e1', h1' |) = progress h1 in
               (| ECase e1' e2 e3, SCase e2 e3 h1' |)
     end
     | TyFst #g #e #t1 #t2 h1 -> begin
          match e with
          | EPair e1 e2 -> (| e1, SFst e1 e2 |)
          | _ -> let (| e', h1' |) = progress h1 in
                 (| EFst e', SFst0 h1' |)
     end
     | TySnd #g #e #t1 #t2 h1 -> begin
          match e with
          | EPair e1 e2 -> (| e2, SSnd e1 e2 |)
          | _ -> let (| e', h1' |) = progress h1 in
                 (| ESnd e', SSnd0 h1' |)
     end
     | TyPair #g #e1 #e2 #t1 #t2 h1 h2 -> 
          if is_value e1 then
               let (| e2', h2' |) = progress h2 in
               (| EPair e1 e2', SPair2 e1 h2' |)
          else 
               let (| e1', h1' |) = progress h1 in
               (| EPair e1' e2, SPair1 h1' e2 |)


(* Typing of substitutions (very easy, actually) *)
let subst_typing #r (s:sub r) (g1:env) (g2:env) =
    x:var{Some? (g1 x)} -> typing g2 (s x) (Some?.v (g1 x))

(* Substitution preserves typing
   Strongest possible statement; suggested by Steven Schäfer *)
let rec substitution (#g1:env) 
                     (#e:exp)
                     (#t:typ)
                     (#r:bool)
                     (s:sub r)
                     (#g2:env)
                     (h1:typing g1 e t)
                     (hs:subst_typing s g1 g2)
   : Tot (typing g2 (subst s e) t)
         (decreases %[bool_order (EVar? e); bool_order r; e])
   = match h1 with
   | TyVar x -> hs x
   | TyLam tlam hbody ->
     let hs'' : subst_typing (sub_inc) g2 (extend tlam g2) =
       fun x -> TyVar (x+1) in
     let hs' : subst_typing (sub_elam s) (extend tlam g1) (extend tlam g2) =
       fun y -> if y = 0 then TyVar y
             else substitution sub_inc (hs (y - 1)) hs''
     in TyLam tlam (substitution (sub_elam s) hbody hs')
      | TyApp hfun harg -> TyApp (substitution s hfun hs) (substitution s harg hs)
   | TyUnit -> TyUnit
   | TyZero -> TyZero
   | TySucc h1 -> TySucc (substitution s h1 hs)
   | TyNRec h1 h2 h3 -> TyNRec (substitution s h1 hs) (substitution s h2 hs) (substitution s h3 hs)
   | TyInl t2 h1 -> 
     let EInl e' = e in
     let hs' : typing g2 (EInl (subst s e')) t = TyInl t2 (substitution s h1 hs) in
     assert (subst s e == EInl (subst s e'));
     hs'
   | TyInr t1 h1 -> 
     let EInr e' = e in
     let hs' : typing g2 (EInr (subst s e')) t = TyInr t1 (substitution s h1 hs) in
     assert (subst s e == EInr (subst s e'));
     hs'
   | TyCase h1 h2 h3 -> TyCase (substitution s h1 hs) (substitution s h2 hs) (substitution s h3 hs)
   | TyFst h1 -> TyFst (substitution s h1 hs)
   | TySnd h1 -> TySnd (substitution s h1 hs)
   | TyPair h1 h2 -> TyPair (substitution s h1 hs) (substitution s h2 hs)

(* Substitution for beta reduction
   Now just a special case of substitution lemma *)
let substitution_beta #e #v #t_x #t #g 
                      (h1:typing g v t_x)
                      (h2:typing (extend t_x g) e t)
  : typing g (subst (sub_beta v) e) t
  = let hs : subst_typing (sub_beta v) (extend t_x g) g =
        fun y -> if y = 0 then h1 else TyVar (y-1) in
    substitution (sub_beta v) h2 hs


(* Type preservation *)
let rec preservation_step #e #e' #g #t (ht:typing g e t) (hs:step e e') 
  : typing g e' t
  =  match hs with
     | SBeta tx e1' e2' -> 
          let TyApp h1 h2 = ht in
          substitution_beta h2 (TyLam?.hbody h1)
     | SApp1 e2' hs1   -> 
          let TyApp h1 h2 = ht in
          TyApp (preservation_step h1 hs1) h2
     | SApp2 e1' hs2   -> 
          let TyApp h1 h2 = ht in
          TyApp h1 (preservation_step h2 hs2)
     | SSucc e' hs1    -> 
          let TySucc h1 = ht in
          TySucc (preservation_step h1 hs1)
     | SNRecV _ _ hs1 ->
          let TyNRec h1 h2 h3 = ht in
          TyNRec (preservation_step h1 hs1) h2 h3
     | SNRec0 _ _ ->
          let TyNRec h1 h2 h3 = ht in
          h2
     | SNRecIter _ _ _ ->
          let TyNRec h1 h2 h3 = ht in
          let TySucc h1' = h1 in
          TyNRec h1' (TyApp h3 h2) h3
     | SInl _ hs1     -> 
          let TyInl t2 h1 = ht in
          TyInl t2 (preservation_step h1 hs1)
     | SInr _ hs1     -> 
          let TyInr t1 h1 = ht in
          TyInr t1 (preservation_step h1 hs1)
     | SCase _ _ hs1 -> 
          let TyCase h1 h2 h3 = ht in
          TyCase (preservation_step h1 hs1) h2 h3
     | SCaseInl _ _ _ -> 
          let TyCase h1 h2 h3 = ht in
          let TyInl _ h1' = h1 in
          TyApp h2 h1'
     | SCaseInr _ _ _ -> 
          let TyCase h1 h2 h3 = ht in
          let TyInr _ h1' = h1 in
          TyApp h3 h1'
     | SFst0 hs1 -> 
          let TyFst h1 = ht in
          TyFst (preservation_step h1 hs1)
     | SFst _ _ -> 
          let TyFst h1 = ht in
          let TyPair h1' _ = h1 in
          h1'
     | SSnd0 hs1 -> 
          let TySnd h1 = ht in
          TySnd (preservation_step h1 hs1)
     | SSnd _ _ -> 
          let TySnd h1 = ht in
          let TyPair _ h1' = h1 in
          h1'
     | SPair1 hs1 _ ->
          let TyPair h1 h2 = ht in
          TyPair (preservation_step h1 hs1) h2
     | SPair2 _ hs2 ->
          let TyPair h1 h2 = ht in
          TyPair h1 (preservation_step h2 hs2)

(** Phil Wadler: Progress + Preservation = Evaluation. **)
let rec eval (gas:nat) (#e:exp) (#t:typ) (ht:typing empty e t)
  : Pure (e':exp & typing empty e' t)
     (requires True)
     (ensures (fun (| e', ht' |) -> True))
     (decreases gas)
  =  if is_value e || gas = 0 then (| e, ht |)
     else let (| e', st |) = progress ht in
          let ht' : typing empty e' t = preservation_step ht st in
          eval (gas-1) ht'

// this lemma is just to show the bug, the lemma does not hold
let lemma_12344 (wt:(wt:exp & typing empty wt (TArr TUnit TNat))) : Lemma (
  eval 1 (TyApp (dsnd wt) TyUnit) == eval 1 (TyApp (dsnd (eval 1 (dsnd wt))) TyUnit)
) by (norm [delta_only [`%eval; `%is_value]; zeta]; dump "H") = ()
@andricicezar andricicezar changed the title Calc produces Memory Leak Normalization loops Feb 12, 2024
@andricicezar
Copy link
Author

Duplicate of #2210.

@andricicezar andricicezar closed this as not planned Won't fix, can't repro, duplicate, stale Feb 12, 2024
@mtzguido
Copy link
Member

mtzguido commented Feb 12, 2024 •
edited

Hi Cezar, this may a different issue. In #2210 there's an explicit norm call using the zeta_full step. In that case, we cannot in general prevent an infinite unfolding during normalization, so I think it can be expected behavior.

There's no such thing here, in the first example you posted, which I minimized slightly to this:

module Bug3207c

(* Minimization of Bug3207.fst *)

open FStar.Tactics
open FStar.Constructive
open FStar.Classical
open FStar.FunctionalExtensionality

(* Constructive-style progress and preservation proof for STLC with
   strong reduction, using deBruijn indices and parallel substitution. *)

type typ =
  | TArr    : typ -> typ -> typ
  | TSum    : typ -> typ -> typ
  | TPair   : typ -> typ -> typ
  | TUnit   : typ
  | TNat    : typ

type var = nat

open FStar.Bytes

type exp =
  | EVar         : var -> exp
  | EApp         : exp -> exp -> exp
  | ELam         : typ -> exp -> exp
  | EUnit        : exp
  | EZero        : exp
  | ESucc        : v:exp -> exp
  | ENRec        : exp -> exp -> exp -> exp
  | EInl         : v:exp -> exp
  | EInr         : v:exp -> exp
  | ECase        : exp -> exp -> exp -> exp
  | EFst         : exp -> exp
  | ESnd         : exp -> exp
  | EPair        : fst:exp -> snd:exp -> exp


(* Type system; as inductive relation (not strictly necessary for STLC) *)

type env = var -> Tot (option typ)

val empty : env
let empty _ = None

(* we only need extend at 0 *)
val extend : typ -> env -> Tot env
let extend t g y = if y = 0 then Some t
                   else g (y-1)

noeq type typing : env -> exp -> typ -> Type =
  | TyVar : #g:env ->
             x:var{Some? (g x)} ->
             typing g (EVar x) (Some?.v (g x))
  | TyLam : #g :env ->
             t :typ ->
            #e1:exp ->
            #t':typ ->
            $hbody:typing (extend t g) e1 t' ->
                   typing g (ELam t e1) (TArr t t')
  | TyApp : #g:env ->
            #e1:exp ->
            #e2:exp ->
            #t11:typ ->
            #t12:typ ->
            $h1:typing g e1 (TArr t11 t12) ->
            $h2:typing g e2 t11 ->
                typing g (EApp e1 e2) t12
  | TyUnit : #g:env ->
             typing g EUnit TUnit
  | TyZero : #g:env ->
             typing g EZero TNat
  | TySucc : #g:env ->
             #e:exp ->
             $h1:typing g e TNat ->
                 typing g (ESucc e) TNat
  | TyNRec : #g:env ->
             #e1:exp ->
             #e2:exp ->
             #e3:exp ->
             #t1:typ ->
             $h1:typing g e1 TNat ->
             $h2:typing g e2 t1 ->
             $h3:typing g e3 (TArr t1 t1) ->
                 typing g (ENRec e1 e2 e3) t1
  | TyInl  : #g:env ->
             #e:exp ->
             #t1:typ ->
             t2:typ ->
             $h1:typing g e t1 ->
                 typing g (EInl e) (TSum t1 t2)
  | TyInr  : #g:env ->
             #e:exp ->
             t1:typ ->
             #t2:typ ->
             $h1:typing g e t2 ->
                 typing g (EInr e) (TSum t1 t2)
  | TyCase : #g:env ->
             #e1:exp ->
             #e2:exp ->
             #e3:exp ->
             #t1:typ ->
             #t2:typ ->
             #t3:typ ->
             $h1:typing g e1 (TSum t1 t2) ->
             $h2:typing g e2 (TArr t1 t3) ->
             $h3:typing g e3 (TArr t2 t3) ->
                 typing g (ECase e1 e2 e3) t3
  | TyFst         : #g:env ->
                    #e:exp ->
                    #t1:typ ->
                    #t2:typ ->
                    $h1:typing g e (TPair t1 t2) ->
                        typing g (EFst e) t1
  | TySnd         : #g:env ->
                    #e:exp ->
                    #t1:typ ->
                    #t2:typ ->
                    $h1:typing g e (TPair t1 t2) ->
                        typing g (ESnd e) t2
  | TyPair        : #g:env ->
                    #e1:exp ->
                    #e2:exp ->
                    #t1:typ ->
                    #t2:typ ->
                    $h1:typing g e1 t1 ->
                    $h2:typing g e2 t2 ->
                        typing g (EPair e1 e2) (TPair t1 t2)

(* Parallel substitution operation `subst` *)
let sub (renaming:bool) = 
    f:(var -> exp){ renaming <==> (forall x. EVar? (f x)) }

let bool_order (b:bool) = if b then 0 else 1

let sub_inc 
  : sub true
  = fun y -> EVar (y+1)

let is_var (e:exp) : int = if EVar? e then 0 else 1

let rec subst (#r:bool)
              (s:sub r)
              (e:exp)
  : Tot (e':exp { r ==> (EVar? e <==> EVar? e') })
        (decreases %[bool_order (EVar? e); 
                     bool_order r;
                     1;
                     e])
  = match e with
  | EVar x -> s x
  | ELam t e1 -> ELam t (subst (sub_elam s) e1)
  | EApp e1 e2 -> EApp (subst s e1) (subst s e2)
  | EUnit -> EUnit
  | EZero -> EZero
  | ESucc e -> ESucc (subst s e)
  | ENRec e1 e2 e3 -> ENRec (subst s e1) (subst s e2) (subst s e3)
  | EInl e -> EInl (subst s e)
  | EInr e -> EInr (subst s e)
  | ECase e1 e2 e3 -> ECase (subst s e1) (subst s e2) (subst s e3)
  | EFst e -> EFst (subst s e)
  | ESnd e -> ESnd (subst s e)
  | EPair e1 e2 -> EPair (subst s e1) (subst s e2)

and sub_elam (#r:bool) (s:sub r) 
  : Tot (sub r)
        (decreases %[1;
                     bool_order r;
                     0;
                     EVar 0])
  = let f : var -> exp = 
      fun y ->
        if y=0
        then EVar y
        else subst sub_inc (s (y - 1))
    in
    introduce not r ==> (exists x. ~ (EVar? (f x)))
    with not_r. 
      eliminate exists y. ~ (EVar? (s y))
      returns (exists x. ~ (EVar? (f x)))
      with (not_evar_sy:squash (~(EVar? (s y)))). 
        introduce exists x. ~(EVar? (f x))
        with (y + 1)
        and ()
    ;
    f

let sub_beta (e:exp)
  : sub (EVar? e)
  = let f = 
      fun (y:var) ->
        if y = 0 then e      (* substitute *)
        else (EVar (y-1))    (* shift -1 *)
    in
    if not (EVar? e)
    then introduce exists (x:var). ~(EVar? (f x))
         with 0 and ();
    f

(* Small-step operational semantics; strong / full-beta reduction is
   non-deterministic, so necessarily as inductive relation *)

type step : exp -> exp -> Type =

let rec is_value (e:exp) : bool = 
     ELam? e || 
     EUnit? e || 
     EZero? e || 
     (ESucc? e && is_value (ESucc?.v e)) || 
     (EInl? e && is_value (EInl?.v e)) ||
     (EInr? e && is_value (EInr?.v e)) || 
     (EPair? e && is_value (EPair?.fst e) && is_value (EPair?.snd e) )

let progress (#e:exp { ~(is_value e) })
                 (#t:typ)
                 (h:typing empty e t)
  : e':exp & step e e'
  =  magic()

(* Typing of substitutions (very easy, actually) *)

(* Type preservation *)
let rec preservation_step #e #e' #g #t (ht:typing g e t) (hs:step e e') 
  : typing g e' t
  =  magic()
  
(** Phil Wadler: Progress + Preservation = Evaluation. **)
let rec eval (#e:exp) (#t:typ) (ht:typing empty e t)
  : Pure (e':exp & typing empty e' t)
     (requires True)
     (ensures (fun (| e', ht' |) -> is_value e'))
  =  if is_value e then (| e, ht |)
     else let (| e', st |) = progress ht in
          let ht' : typing empty e' t = preservation_step ht st in
          admit (); (** TODO: proof of termination required **)
          eval ht'

type wholeT = wt:exp & typing empty wt (TArr TUnit TNat)

#set-options "--debug Bug3207c --debug_level Rel,NormTop"

let naive_rel_implies_c (wt : wholeT)  =
  let (| ew, htw |) = wt in
  calc (==) {
    eval (TyApp (dsnd (eval htw)) TyUnit);
  }

The problem is that the unifier needs at some point to solve whether eval (TyApp (dsnd (eval htw)) TyUnit) is equal to "itself", but one of the happens to have its universes levels instantiated and the other does not (I don't know why yet). Then we go into a unifier heuristic that tries to equate both sides by a normalizer "blast", with zeta on (no Exclude Zeta in the steps, internally zeta is on by default)

FStar/src/typechecker/FStar.TypeChecker.Rel.fst

Lines 4236 to 4254 in 10183ea

let equal t1 t2 : bool =
(* Try comparing the terms as they are. If we get Equal or NotEqual,
we are done. If we get an Unknown, attempt some normalization. *)
let r = U.eq_tm t1 t2 in
match r with
| U.Equal -> true
| U.NotEqual -> false
| U.Unknown ->
let steps = [
Env.UnfoldUntil delta_constant;
Env.Primops;
Env.Beta;
Env.Eager_unfolding;
Env.Iota ] in
let env = p_env wl orig in
let t1 = norm_with_steps "FStar.TypeChecker.Rel.norm_with_steps.2" steps env t1 in
let t2 = norm_with_steps "FStar.TypeChecker.Rel.norm_with_steps.3" steps env t2 in
U.eq_tm t1 t2 = U.Equal
in

This heuristic is somewhat suspect, since it can cause loops as we see here, but it's also useful to equate things like ty ([] @ l) with ty l without using the SMT solver (@ is recursive). I tried disabling it, which leads to some small but acceptable regressions in the F* repo, but more significant ones in steel which I haven't fully resolved.

Let's keep this open to decide whether we should keep zeta in this heuristic or not. There's also the question of why the universes don't match, which would make the unifier call trivial.

@mtzguido mtzguido reopened this Feb 12, 2024
@mtzguido
Copy link
Member

Ah, this is why it's looping. The is_value function is recursive, but the recursion is not guarded under a match.

let rec is_value (e:exp) : bool = 
     ELam? e || 
     EUnit? e || 
     EZero? e || 
     (ESucc? e && is_value (ESucc?.v e)) || 
     (EInl? e && is_value (EInl?.v e)) ||
     (EInr? e && is_value (EInr?.v e)) || 
     (EPair? e && is_value (EPair?.fst e) && is_value (EPair?.snd e) )

In this case, when F* has to unfold is_value, it will encounter is_value again in its definition and possibly keep unfolding. To prevent this in most cases, we have a heuristic in the normalizer preventing the unfolding of a recursive function under a match, which is the common case for recursive occurrences in definitions. Defining is_value like so:

let rec is_value (e:exp) : bool = 
  match e with
  | ELam _  _
  | EUnit 
  | EZero -> true
  | ESucc e -> is_value e
  | EInl e -> is_value e
  | EInr e -> is_value e 
  | EPair e1 e2 -> is_value e1 && is_value e2
  | _ -> false

Makes this work reliably.

I would still keep this open for findind out why there's a universe mismatch.

mtzguido added a commit to mtzguido/FStar that referenced this issue Feb 13, 2024
@mtzguido
Add FStarLang#3207 files to regression suite, don't close issue yet
f4dd99a
@mtzguido mtzguido mentioned this issue Feb 13, 2024
Merged
@mtzguido
Copy link
Member

mtzguido commented Feb 13, 2024 •
edited

OK I figured why the universes were different: they weren't. The pretty printer was not showing them correctly, it was showing a resolved uvar as unknown. Similarly, the eq_tm function above would not consider a resolved uvar to be equal to its solution, so the call failed and we attempted normalization. This will be fixed by #3216, and these examples now pass.

I would keep this open for thinking about whether it's wise for the unifier to do zeta.

@mtzguido mtzguido changed the title Normalization loops Unifier causing normalization loops (zeta enabled in equal heuristic) Feb 13, 2024
mtzguido added a commit that referenced this issue Feb 13, 2024
@mtzguido
Merge pull request #3216 from mtzguido/3207
7579c2d 
Some fixes related to #3207
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@andricicezar @mtzguido