Soundness: `U.term_eq` ignores a computation type's pre/postcondition, so the VC simplifier rewrites a false implication to `True`

[hei411]

Summary

A plain .fst file proves False on default options, with no assume,
admit, magic, --ext, #push-options, expect_failure, friend or
__no_positivity.

FStarC.Syntax.Util.term_eq decides syntactic equality of two arrow types by
comparing their binders and then their computation types. The computation
comparison, comp_eq_dbg, looks at only the effect name and the result
type — it never looks at the effect arguments, i.e. at the pre- and
postcondition. So these two types are reported equal:

unit -> Lemma (ensures True)     // inhabited by (fun () -> ())
unit -> Lemma (ensures False)    // empty

The VC simplifier then rewrites p ==> q to True whenever
U.term_eq p q holds, and likewise for p <==> q. Instantiating p and q
with two propositions that differ only inside such a computation type yields
an implication that F* discharges without Z3 ever seeing it, even though the
hypothesis is true and the conclusion is false. Composing it with an
ordinary proof of the hypothesis gives False.

Repro 1 — the minimal witness

F* accepts both of these, and both are plainly false: the hypothesis is
vacuously true because unit -> Lemma False is empty, and the conclusion is
false because fun () -> () inhabits unit -> Lemma True.

module CompEqMinimal

let imp = assert_norm ( (forall (f: (unit -> Lemma False)). False)
                    ==> (forall (f: (unit -> Lemma True)). False) )

let iff = assert_norm ( (forall (f: (unit -> Lemma False)). False)
                   <==> (forall (f: (unit -> Lemma True)). False) )

$ fstar.exe CompEqMinimal.fst
Verified module: CompEqMinimal
All verification conditions discharged successfully

Repro 2 — False

The two arrow types are placed behind abbreviations. That is not cosmetic:
assert_norm delta-unfolds them, so the rewrite fires and bridge is
accepted; but the VC simplifier at the use site does not unfold them, so
the false implication survives as a hypothesis in bad instead of being
rewritten to True a second time.

module CompEqPostcondFalse

let ta : Type0 = unit -> Lemma True
let tb : Type0 = unit -> Lemma False

(* `tb` is empty ... *)
let step (f: tb) : Lemma False = f ()
let lhs () : Lemma (forall (f: tb). False) = FStar.Classical.forall_intro step

(* ... and `ta` is not, so this implication is false. *)
let bridge () : Lemma ((forall (f: tb). False) ==> (forall (f: ta). False))
  = assert_norm ((forall (f: tb). False) ==> (forall (f: ta). False))

let elim (g: ta) : Lemma (requires forall (f: ta). False) (ensures False) = ()

let bad () : Lemma False =
  lhs ();
  bridge ();
  elim (fun () -> ())

let one_is_zero () : Lemma (1 == 0) = bad ()
let anything (a:Type) : a = bad (); false_elim ()

$ fstar.exe CompEqPostcondFalse.fst
Verified module: CompEqPostcondFalse
All verification conditions discharged successfully

CompEqPostcondIff.fst is the same proof routed through the <==> rewrite
instead of the ==> rewrite; it also verifies with no errors.

Negative control

Identical to repro 2 except that the two arrow types differ in their effect
name, which comp_eq_dbg does compare. Both result types are unit.
This is correctly rejected, which confirms the proof turns on the
postcondition being discarded and not on the shape of the argument.

module CompEqEffectControl

let ta : Type0 = unit -> Ghost unit (requires True) (ensures fun _ -> True)
let tb : Type0 = unit -> Lemma False

let bridge () : Lemma ((forall (f: tb). False) ==> (forall (f: ta). False))
  = assert_norm ((forall (f: tb). False) ==> (forall (f: ta). False))

$ fstar.exe CompEqEffectControl.fst
* Error 19 at CompEqEffectControl.fst(9,4-9,15):
  - Assertion failed

A second control in which ta and tb are given the same definition is
accepted, as it should be: there the implication really is true.

Root cause

src/syntax/FStarC.Syntax.Util.fst, in term_eq_dbg:

| Tm_arrow {b=b1;comp=c1}, Tm_arrow {b=b2;comp=c2} ->
  (check "arrow binders" (binder_eq_dbg dbg b1 b2)) &&
  (check "arrow comp"    (comp_eq_dbg dbg c1 c2))

and comp_eq_dbg itself:

and comp_eq_dbg (dbg : bool) (c1 c2 : comp) : ML bool =
    let eff1, res1 = comp_eff_name_and_res c1 in
    let eff2, res2 = comp_eff_name_and_res c2 in
    (check_term_eq dbg "comp eff"  (lid_equals eff1 eff2)) &&
    //(check "comp univs"  (c1.comp_univs = c2.comp_univs)) &&
    (check_term_eq dbg "comp result typ"  (term_eq_dbg dbg res1 res2)) &&
    true //eq_flags c1.flags c2.flags

comp_eff_name_and_res projects exactly two components out of a Comp
node. The remaining fields of comp_typ — in particular effect_args,
which is where Lemma's pre- and postcondition live, and comp_univs,
whose comparison is commented out — are simply not examined. Two Comp
nodes with the same effect name and result type are therefore always equal
according to term_eq, however different their specifications.

Why that is fatal rather than merely imprecise

Most callers of term_eq compare terms that typing already forces to be
equal, so a false positive is invisible. Two callers do not, and they use
the answer to decide a logical question outright.
src/typechecker/FStarC.TypeChecker.TermEqAndSimplify.fst, in simplify:

else if S.fv_eq_lid fv PC.imp_lid
then match args |> List.map simplify with
     | [_; (Some true, _)]
     | [(Some false, _); _] -> w U.t_true
     | [(Some true, _); (_, (arg, _))] -> maybe_auto_squash arg
     | [(_, (p, _)); (_, (q, _))] ->
       if U.term_eq p q
       then w U.t_true
       else squashed_head_un_auto_squash_args tm

and the same three lines again in the iff_lid branch. p and q here are
two arbitrary user propositions; nothing constrains them to be equal. When
term_eq wrongly answers true, the implication is replaced by True
before the SMT solver is invoked, so there is no second line of defence —
Z3 is never asked, and the mirrored rules in
FStarC.TypeChecker.Normalize.fst behave the same way.

Note that this is specifically a defect of U.term_eq, not of the other
syntactic-equality function in the same subsystem. eq_tm, in the same file
as simplify, has an eq_comp that compares comp_univs, effect_name,
result_typ and both comp_pre and comp_post, and it returns a
three-valued eq_result so that an inconclusive comparison degrades to
Unknown rather than to a positive answer. The correct behaviour is
therefore already implemented a few hundred lines above the two rewrite
rules that do not use it.

Suggested fix

Either compare effect_args in comp_eq_dbg (and re-enable the
commented-out comp_univs check), or change the imp_lid/iff_lid
branches of simplify — and their counterparts in Normalize.fst — to use
eq_tm ... = Equal rather than U.term_eq, so that anything the comparison
cannot settle falls through to Z3.

The first is the narrower fix but changes the meaning of term_eq
everywhere it is used; the second is local to the two rules that actually
draw a logical conclusion from the answer.

Related, but distinct

• Soundness: the VC simplifier judges an empty function type inhabited, proving False #4485 is a different defect in the same simplifier:
  clearly_inhabited decides an arrow type's inhabitation from its result
  type alone. That one is about a whitelist of base types and fires through
  the forall/exists rules; this one is about comp_eq_dbg dropping the
  effect arguments and fires through the ==>/<==> rules. Fixing either
  leaves the other open — the negative control above uses unit, which is
  not in the clearly_inhabited whitelist, and the live repro's rewrite
  happens at a Tm_app whose head is l_imp, not a quantifier.
• Some problems with reflection and simplification of equalities #2806 is about eq_tm on constants; the file it hardened
  is the other equality function, the one that is not used here.
• Error message with equal types: we shoud print effect arguments or a hint if types are otherwise equal. #1225 asks for better error messages when two types differ
  only in their effect arguments, which is the same blind spot surfacing as
  a usability problem rather than a soundness one.

Environment

F* 2026.08.23   platform=Linux_x86_64   (also reproduced on F* nightly-2026-08-17)

Both cited source files are byte-identical to master at the time of
writing. All four files above were checked on both builds: the two False
proofs and the minimal witness report 0 errors on each, and the effect-name
control reports Error 19 on each.

[nikswamy]

This is addressed by #4515. Computation types now only have a result type, no longer any other indices. To be confirmed that the issues no longer repro and then close.