fix(fel): require per-step weights non-negative over the counter range

examples/ChaChaPoly/chacha_poly.ec

@@ -2257,7 +2257,9 @@ section PROOFS.
       inline*; wp; rnd; auto=> &h /> *.
       by apply pr_TPI_ok_filter=> //=.
     + by move=> c; proc; sp; inline*; sp; if; auto=> /#.
-    + by move=> b c; proc; inline*; sp; rcondf 1; auto. 
+    + by move=> b c; proc; inline*; sp; rcondf 1; auto.
+    + (* F003: non-negativity of the per-step weight over the whole range *)
+      by move=> i; smt(size_ge0 ge0_pr_zeropol).
     + (* compute sum of probabilities *)
       have hn1: n1 = size (filter (fun n => (n, C.ofintd 0) \in roout) (map (fun (c:ciphertext) => c.`1) l)).
       + by rewrite /n1 !size_filter count_map /preim.
@@ -2294,6 +2296,8 @@ section PROOFS.
     + move=> c; proc; inline*; sp; rcondt 1; 1: auto=> />.
       by wp -1=> />; conseq(:_==> true); auto; smt().
     + by move=> b c; proc; inline*; sp; rcondf 1; auto=> />.
+    + (* F003: non-negativity of the per-step weight over the whole range *)
+      by move=> i; smt(size_ge0 mu_bounded).
     + have hn2: n2 = size (filter (fun n => (n, C.ofintd 0) \notin roout) (map (fun (c:ciphertext) => c.`1) l)).
       + by rewrite /n2 !size_filter count_map /preim.
       rewrite -BRA.mulr_suml ler_wpmul2r; 1:smt(mu_bounded).
@@ -2734,7 +2738,9 @@ section PROOFS.
     rcondt 2; 1: auto; wp=> />; rnd=> />; skip=> /> &hr *.
     by have <- //=:=dpoly_out_funi witness ti{hr}.
   + move=> c; proc; auto=> />; smt().
-  by move=> b c; proc; auto.
+  + by move=> b c; proc; auto.
+  (* F003: non-negativity of the per-step weight over the whole range *)
+  by move=> i; smt(mu_bounded).
   qed.
 
 

examples/Upto.ec

@@ -142,4 +142,6 @@ move=> b c; proc; sp; if=> //.
 swap 1 1; wp.
 exists* Experiment.WO.cO; elim* => cO.
 by call (hf2 cO); auto=> /> /#.
+(* F003: non-negativity of the per-step weight over the whole range *)
+by move=> i; move: (hg i); smt().
 qed.

examples/prg-tutorial/PRGc.ec

@@ -523,6 +523,8 @@ section Lemma1.
   (* When condition does not hold, the counter value does not decrease
      and bad is not triggered *)
   done.
+  (* F003: non-negativity of the per-step weight over the whole range *)
+  by move=> i; smt(mu_bounded).
   qed.
 end section Lemma1.
 

src/phl/ecPhlFel.ml

@@ -157,6 +157,22 @@ let t_failure_event_r (at_pos, cntr, ash, q, f_event, pred_specs, inv) tc =
     f_real_le v bd
   in
 
+  (* Soundness side-condition: the per-step failure weight [ash] must be
+     non-negative over the WHOLE counter range [0, q).  The bound proven by
+     [fel] is the sum of [ash] over the full range, which must dominate the
+     sum over the counter values actually visited.  Without this obligation a
+     counter that jumps (skipping indices) combined with negative weights at
+     the skipped indices makes the full-range sum smaller than the visited
+     sum, which is unsound (e.g. weights (1, -1) with a 0 -> 2 jump would let
+     [fel] "prove" Pr[bad] <= 0). *)
+  let nonneg_goal =
+    let i_id = EcIdent.create "i" in
+    let i    = f_local i_id tint in
+    let hyp  = f_and (f_int_le f_i0 i) (f_int_lt i q) in
+    let body = f_real_le f_r0 (f_app_simpl ash [i] treal) in
+    f_forall_simpl [i_id, GTty tint] (f_imp hyp body)
+  in
+
   (* we must quantify over memories *)
   let post_goal =
     let lev = map_ss_inv2 f_and f_event (map_ss_inv1 (fun cnt -> f_int_le cnt q) cntr) in
@@ -246,7 +262,10 @@ let t_failure_event_r (at_pos, cntr, ash, q, f_event, pred_specs, inv) tc =
   let os_goals =
     List.concat (List.map oracle_goal (Sx.ntr_elements os)) in
 
-  let concls = bound_goal :: post_goal :: init_goal :: os_goals in
+  (* [nonneg_goal] is placed LAST so that existing [fel] proof scripts keep
+     their subgoals (bound, post, init, oracles) in the same positions; the
+     new obligation simply surfaces as a trailing goal. *)
+  let concls = bound_goal :: post_goal :: init_goal :: os_goals @ [nonneg_goal] in
   let res = FApi.xmutate1 tc (`Fel (cntr, ash, q, f_event, pred_specs)) concls in
   res
 

tests/fel-counter-jump.ec

@@ -0,0 +1,38 @@
+(* Regression for the `fel` counter-jump / negative-weight bug.
+
+   The failure-event lemma tactic used to accept a counter that JUMPS (skipping
+   indices) combined with NEGATIVE per-step weights at the skipped indices. The
+   full-range weight sum could then be made smaller than the sum over the
+   counter values actually visited, letting `fel` "prove" Pr[bad] <= 0 for an
+   event that in fact happens with probability 1.
+
+   Here the counter jumps 0 -> 2 (index 1 is never visited) and the weight
+   ash = (fun x => if x = 0 then 1 else -1) is negative at the skipped index 1,
+   giving whole-range sum 1 + (-1) = 0.
+
+   The fixed tactic emits an extra obligation `forall i, 0 <= i < q => 0 <= ash i`
+   (unprovable here since ash 1 = -1). The old discharge script covers only the
+   original goals, so the whole `by fel ...` closing must now fail. *)
+require import AllCore List Distr DBool FelTactic StdBigop.
+(*---*) import Bigreal.
+(*---*) import List.Range.
+
+module M = {
+  var bad : bool
+  var c   : int
+
+  proc o() : unit = { if (c = 0) { bad <- true; c <- 2; } }
+  proc f() : unit = { bad <- false; c <- 0; o(); }
+}.
+
+lemma pr_le0 &m : Pr[M.f() @ &m : M.bad] <= 0%r.
+proof.
+fail (by fel 2 M.c (fun x => if x = 0 then 1%r else (-1)%r) 2 M.bad [M.o : (M.c = 0)] (0 <= M.c /\ M.c <= 2);
+  [ (have -> : range 0 2 = [0; 1] by rewrite range_ltn // range_ltn // range_geq //);
+    rewrite BRA.big_cons BRA.big_cons BRA.big_nil /predT /=
+  | move=> &hr; smt()
+  | auto
+  | proc; rcondt 1; auto
+  | move=> c0; proc; auto=> /#
+  | move=> b0 c0; proc; auto=> /# ]).
+abort.

theories/crypto/Birthday.eca

@@ -78,6 +78,8 @@ section.
       apply (Mu_mem.mu_mem_le_size (Sample.l{hr}) uT (mu1 uT maxu)). 
       by move=> x _;rewrite maxuP.
     by move=> c; proc; auto=> /#.
+    (* F003: non-negativity of the per-step weight over the whole range *)
+    by move=> i; smt(mu_bounded).
   qed.
 
   lemma pr_Sample_le_q2 &m:

theories/crypto/PROM.ec

@@ -303,6 +303,8 @@ fel 1 (fsize RO.m) (fun x => x%r * Pc) q (fcoll f RO.m)
   by move: j_in_mVx; rewrite j_neq_x=> /= -> /=.
 - move => c; proc; auto => />; smt(get_setE fsize_set).
 - move => b c; proc; by auto.
+(* F003: non-negativity of the per-step weight over the whole range *)
+- by move=> i; smt(Pc_ge0).
 qed.
 
 end section Collision.

theories/crypto/RndExcept.eca

@@ -290,6 +290,8 @@ abstract theory AdversaryN.
       by rcondt 1 => //;wp;conseq (_: _ ==> true) => // /#.
     move=> b c;proc;sp;inline *;if => //.
     sp;wp;if;auto => /#.
+    (* F003: non-negativity of the per-step weight over the whole range *)
+    by move=> i; smt(p_pos n_pos).
   qed.
 
   local lemma pr_bad_eq &m :

theories/crypto/prp_prf/Strong_RP_RF.eca

@@ -487,6 +487,8 @@ section CollisionProbability.
       by rewrite !fdom_set !fcardU !fcard1; smt(fcard_ge0).
     * by auto=> /#.
   + by move=> b c; proc; rcondf 2; auto.
+  (* F003: non-negativity of the per-step weight over the whole range *)
+  + by move=> i; smt(mu_bounded).
   qed.
 end section CollisionProbability.