`fel` + `smt`: internal assertion (ecSmt.ml `assert has_locals`) when the `Pr` event mentions `res`

[sociofabric]

Summary

smt raises an internal assertion, rather than failing or erroring, on the
subgoal fel produces when the target Pr[...] event mentions res:

[critical] anomaly: File "src/ecSmt.ml", line 909, characters 5-11: Assertion failed

Reproduced on main at 87b6f8b (2026-07-25), built from a clean clone with
opam install ./easycrypt.opam --deps-only && dune build. Plain module type
throughout — no quantum extensions involved.

Reproducer

require import AllCore Distr List FelTactic.
require import StdBigop StdOrder.
(*---*) import Bigreal.BRA StdOrder.RealOrder.

type T.
op [lossless] d : T distr.
op q : int.
axiom q_ge0 : 0 <= q.

module type O = { proc f(x : T) : bool }.
module type A (P : O) = { proc go() : unit { P.f } }.

module G (Adv : A) = {
  var bad : bool
  var c   : int

  module P : O = {
    proc f(x : T) : bool = {
      var r;
      if (c < q) {
        c <- c + 1;
        r <$ d;
        if (r = witness) { bad <- true; }
      }
      return bad;
    }
  }

  proc main() : bool = {
    bad <- false;
    c   <- 0;
    Adv(P).go();
    return bad;
  }
}.

section.
declare module Adv <: A { -G }.

lemma L &m : Pr[G(Adv).main() @ &m : res] <= q%r * mu1 d witness.
proof.
fel 2 G.c (fun _ => mu1 d witness) q G.bad [G(Adv).P.f : (G.c < q)] (G.c <= q).
admit.
smt().          (* <-- anomaly *)
admit.
admit.
admit.
admit.
qed.
end section.

What isolates it

variation	result
as above	anomaly
Pr[... : res] → Pr[... : G.bad], one token, nothing else changed	accepted
smt() → admit.	accepted

So the six goals fel produces are well-formed — the failure is in the SMT
translation of one of them — and the trigger is specifically res, not fel
and not the surrounding development. (fel's first goal is the arithmetic sum
bound and smt discharges it without complaint.)

It also reproduces identically on the older deploy-quantum-upgrade branch
(3cef12a), where the same assertion is at ecSmt.ml:900.

Diagnosis

src/phl/ecPhlFel.ml builds the second subgoal as

forall &m0, ev{m0} => inv{m0} => bad{m0} /\ cntr{m0} <= q

and quantifies the memory using the memtype of the ambient memory of the
Pr:

let pr_m = oget (Memory.byid pr.pr_mem env) in
...
let m = (EcIdent.create "&hr", snd pr_m) in

That memtype has no locals. When ev mentions res — a local — the
translation reaches trans_mem's assert has_locals (src/ecSmt.ml:909) and
aborts.

Substituting the Pr memtype, which declares res and which trans_pr
already uses for exactly this purpose, removes the anomaly:

-    let m = (EcIdent.create "&hr", snd pr_m) in
+    let m = (EcIdent.create "&hr",
+             snd (EcEnv.Fun.prF_memenv (EcIdent.create "&hr") f env)) in

Built against 87b6f8b, the reproducer then fails with an ordinary
cannot prove goal (strict) instead of the assertion.

What the right fix might be instead

I am not proposing that diff as a fix — it is offered as evidence for the
diagnosis. Even with it, the goal is not provable when the event is res: in
the quantified memory res is an unconstrained local, so nothing links it to
bad. fel appears to want a global bad event, which is what every use
in examples/ does (examples/Upto.ec, examples/ChaChaPoly,
examples/prg-tutorial). If that is the intended contract, rejecting the
input up front with a message to that effect would be more useful than either
the assertion or an unprovable subgoal — the assertion is what cost the time
here, because an internal error reads as "the tactic is broken" rather than
"the goal is stated wrongly".

Workaround

State the bad event over module globals. The same bound then goes through with
all six goals discharged.

[sociofabric]

Corrections to the original report

I put this report through an adversarial re-check and found four inaccuracies of my own. The core defect and the diagnosis stand; the recommendation did not, and that is the part a maintainer would have acted on. Apologies for the noise.

1. "Reject events mentioning res" is wrong advice — please disregard it

I wrote that the subgoal is "not provable when the event is res" and suggested rejecting such inputs up front. That generalises from res alone to every event mentioning res, and it is false.

With the diff below applied to main 87b6f8b:

lemma L &m : Pr[G(Adv).main() @ &m : res /\ G.bad] <= q%r * mu1 d witness.

is accepted — the second subgoal becomes
res{hr} /\ G.bad{hr} => G.c{hr} <= q => G.bad{hr} /\ G.c{hr} <= q, which smt() closes, and the whole six-goal development goes through. Only the bare res event stays unprovable, and correctly so, since nothing then links res to the bad event.

That matters because Pr[… : res /\ bad] is an ordinary up-to-bad shape. Rejecting events that mention res would reject sound statements.

So the fix I would now suggest is just the memtype one: give fel's memory binder the Pr memtype (EcEnv.Fun.prF_memenv), the same one trans_pr uses. No input rejection.

(Verified both directions on 87b6f8b, patched and unpatched. Watch out for stale .eco files when flipping between builds — a cached success from the patched run masked the unpatched anomaly for me until I deleted it.)

2. "The six goals are well-formed" is not supported by the evidence I gave

I inferred well-formedness from admit. being accepted. admit closes any goal, so it shows nothing of the kind — and it contradicts my own diagnosis, which blames ecPhlFel.ml (and my patch changes ecPhlFel.ml, not ecSmt.ml). The goal really is malformed: the binder carries a memtype with no locals and the body then dereferences res in that memory. The assertion in trans_mem is arguably doing its job; the bug is upstream of it.

3. "fel's first goal … smt discharges it without complaint" — overstated

smt() alone does not close goal 1; it returns an ordinary cannot prove goal (strict) (it needs the sumr_const / count_predT / size_range rewrite chain first). The claim I should have made, which still isolates the trigger, is: goal 1 fails without an anomaly. The distinction between "ordinary proof failure" and "internal assertion" is the whole point, and I blurred it.

4. The diff as posted will not build under your CI profile

It orphans pr_m (ecPhlFel.ml:129), whose only consumer was the line being replaced — the later pr_m at :181 is a shadowing rebinding. Under --profile ci (-warn-error +a) that is warning 26. Rename to _pr_m, or inline the oget.

---

Unchanged and re-verified: the anomaly itself, the site (ecSmt.ml:909 on main, :900 on deploy-quantum-upgrade), the causal chain through the ambient memtype, the fact that it is not quantum-specific, and that every fel in examples/ targets a global bad event.