Skip to content

[chore] fix unused unfold warnings #1042

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

Merged
fdupress merged 1 commit into from
Jun 12, 2026
Merged

[chore] fix unused unfold warnings #1042

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions examples/MEE-CBC/FunctionalSpec.ec
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -466,7 +466,7 @@ phoare mee_encrypt_correct _mk _ek _p _c:
proof.
have->: mu1 (dapply (fun iv=> iv :: mee_enc AES hmac_sha256 _ek _mk iv _p) dblock) _c
= mu1 (dmap dblock (fun iv=> iv :: mee_enc AES hmac_sha256 _ek _mk iv _p)) _c by move.
rewrite dmap1E /preim /pred1 /=.
rewrite dmap1E /pred1 /=.
proc; inline MAC.tag PRPc.PseudoRP.f.
swap 6 -5 => //=; alias 2 iv = s.
while ( 0 <= i <= size (pad _p (hmac_sha256 _mk _p))
Expand Down Expand Up @@ -528,7 +528,7 @@ conseq (_: true ==> true) (_: _ ==> _)=> //=.
rewrite (ler_asym (size p) (size (behead _c)) _);
rewrite ?ge_szc_p ?le_szc_p // take_size => p_def.
split.
+ case: {-1}(unpad p) (eq_refl (unpad p))=> //= @/mee_cbc - [] m t.
+ case: {-1}(unpad p) (eq_refl (unpad p))=> //= - [] m t.
by rewrite /mee_dec /= -p_def=> -> /=.
by rewrite /mee_dec -p_def /= => ->.
proc; inline *; wp; while true (size c - i); auto =>/#.
Expand Down
2 changes: 1 addition & 1 deletion examples/SchnorrPK.ec
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -126,7 +126,7 @@ section SchnorrPKSecurity.
rewrite /R /R_DL; move => sigmarel.
byphoare (_: h = x /\ w' = w ==> _) => //; rewrite sigmarel.
proc; inline*; swap 3 -2; swap 8 -7.
wp; rewrite /snd /=; auto => &hr />.
auto=> &hr />.
by rewrite dt_ll => /> *; algebra.
qed.

Expand Down
14 changes: 7 additions & 7 deletions examples/UC/dh_enc.ec
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1028,7 +1028,7 @@ wp; call (_:
+ by move => *; inline *;auto => /#.
(* Backdoor F2Auth *)
move=> m2 p; inline *; auto => /> &1 &2.
rewrite /staterel /leak oget_some /unblock /kstp /rcv.
rewrite /staterel /leak oget_some /rcv.
by case (FKE.st{2}.`kst) => /> /#.

(* WRAP-UP CALL *)
Expand Down Expand Up @@ -1712,11 +1712,11 @@ call (_: invotp OTP.Initiator.p{1}
sp 1 0; if{1}.
(* STEP INITIATOR *)
+ sp 0 1; match{2}.
+ by rcondf {1} 1; auto => /> &1;rewrite /invotp /kstp; smt().
+ rcondt {1} 1; first by auto => /> &1;rewrite /invotp /kstp; smt().
by sp 1 0; match{1}; by move => *;rcondf {1} 5; auto => /> &1;rewrite /invotp /kstp;smt().
+ rcondt {1} 1; first by auto => /> &1;rewrite /invotp /kstp;smt().
by sp 1 0; match{1}; by move => *;rcondf {1} 5; auto => /> &1;rewrite /invotp /kstp;smt().
+ by rcondf {1} 1; auto => /> &1;rewrite /invotp; smt().
+ rcondt {1} 1; first by auto => /> &1;rewrite /invotp; smt().
by sp 1 0; match{1}; by move => *;rcondf {1} 5; auto => /> &1;rewrite /invotp;smt().
+ rcondt {1} 1; first by auto => /> &1;rewrite /invotp;smt().
by sp 1 0; match{1}; by move => *;rcondf {1} 5; auto => /> &1;rewrite /invotp;smt().
+ rcondt {2} 1; first by move => *; wp;skip;smt().
if{1}.
+ seq 0 3 : (#pre /\ (oget (getl (oget lfa{2}))) = Ch_Init);
Expand Down Expand Up @@ -1769,7 +1769,7 @@ call (_: invotp OTP.Initiator.p{1}
seq 0 3 : (#pre /\ (oget (getl (oget lfa{2}))) <> Ch_Init);
first by wp;skip;smt().
by match {2}; 1: (by exfalso => /#); auto => /#.
by rcondf{1} 1; [ by auto => /> &1;rewrite /invotp /kstp;smt()| by auto=> />].
by rcondf{1} 1; [ by auto => /> &1;rewrite /invotp;smt()| by auto=> />].
(* STEP RESPONDER *)
sp 0 1; match{2}; first 3 by auto;rewrite /invotp /#.
+ by rcondf{2} 1; auto; rewrite /invotp /#.
Expand Down
6 changes: 3 additions & 3 deletions theories/algebra/DynMatrix.eca
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1335,7 +1335,7 @@ qed.

lemma mul_colmxc (v:vector) c: (colmx v) *^ vectc 1 c = c ** v.
proof.
rewrite eq_vectorP size_scalarv size_mulmxv /= /max 1:// => i bound.
rewrite eq_vectorP size_scalarv size_mulmxv /= 1:// => i bound.
rewrite get_scalarv get_mulmxv dotpE /= /max /=.
by rewrite Big.BAdd.big_int1 /= get_vectc // mulrC.
qed.
Expand Down Expand Up @@ -1826,7 +1826,7 @@ lemma dmatrix1E d m : mu1 (dmatrix d (rows m) (cols m)) m =
BRM.bigi predT (fun j => mu1 d m.[i, j]) 0 (cols m)) 0 (rows m).
proof.
pose g (m: matrix) := mkseq (fun i => col m i) (cols m).
rewrite (in_dmap1E_can _ _ g) /ofcols.
rewrite (in_dmap1E_can _ _ g) 1,2:/ofcols.
- rewrite /g eq_matrixP /= => i j bound.
by rewrite get_offunm /= 1:/# nth_mkseq 1:/# get_col.
- rewrite /g => y y_in <- /=.
Expand Down Expand Up @@ -1902,7 +1902,7 @@ proof.
move => k_ge0; rewrite /dmatrix /ofcols ler_maxr // dlist1 dmap_comp /(\o).
apply eq_dmap_in => v /size_dvector; rewrite ler_maxr //= => s_v.
rewrite /colmx s_v; apply/eq_matrixP => /= i j [i_bound j_bound].
by rewrite /ofcols !get_offunm /#.
by rewrite !get_offunm /#.
qed.

lemma supp_dmatrix d m r c :
Expand Down
12 changes: 6 additions & 6 deletions theories/algebra/PolyReduce.ec
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -67,7 +67,7 @@ proof.
move=> p un_p; rewrite ideal_eq1P 1:&(idI) //; apply/negP.
move/fun_ext => /(_ poly1); rewrite mem_idT /I mem_idgen1.
case/eqT=> q /(congr1 deg); rewrite deg1 => /eq_sym.
case: (q = poly0) => [->|nz_q]; first by rewrite /( * ) mul0r deg0.
case: (q = poly0) => [->|nz_q]; first by rewrite mul0r deg0.
rewrite degM_proper; 1: by rewrite lc_polyXnDC // mulr1 lc_eq0.
rewrite deg_polyXnDC // -!addrA /= gtr_eqF //.
by rewrite (_ : 1 = 1 + 0) 1:// ler_lt_add // deg_ge1.
Expand Down Expand Up @@ -126,7 +126,7 @@ proof. by rewrite /( ** ) !scalepE -2!mulE reprK. qed.

(* -------------------------------------------------------------------- *)
lemma eqv_Xn : eqv (exp X n) (-poly1).
proof. rewrite eqv_sym /eqv /[-] opprK /I mem_idgen1_gen. qed.
proof. rewrite eqv_sym /eqv opprK /I mem_idgen1_gen. qed.

(* -------------------------------------------------------------------- *)
op reduce (p : poly) : poly =
Expand Down Expand Up @@ -165,7 +165,7 @@ rewrite {1}(polyE p) /reduce !PCA.big_seq &(eqv_sum) /=.
move=> i /mem_range [rg_i _]; rewrite mulrC -scalepA.
pose q := exp X (i %/ n * n) * exp X (i %% n).
rewrite !scalepE &(eqvMl) &(eqv_trans q).
- rewrite (_ : q = exp X i) // /q /( * ) -exprD_nneg // -?divz_eq //.
- rewrite (_ : q = exp X i) // /q -exprD_nneg // -?divz_eq //.
- by rewrite mulr_ge0 // divz_ge0.
- by rewrite modz_ge0 gtr_eqF.
apply/eqvMr; rewrite -polyCX ?divz_ge0 // (IntID.mulrC _ n).
Expand All @@ -192,7 +192,7 @@ split=> [eq_rd|eqv_pq].
have @/eqv @/I: eqv (reduce p) (reduce q).
- by rewrite !(eqv_reducel, eqv_reducer).
case/mem_idgen1=> r /(congr1 deg); case: (r = poly0) => [->>|nz_r].
- by rewrite /( * ) mul0r deg0 deg_eq0 subr_eq0 => ->.
- by rewrite mul0r deg0 deg_eq0 subr_eq0 => ->.
have: deg (reduce q - reduce p) <= n.
- by rewrite &(ler_trans _ _ _ (degB _ _)) ler_maxrP !deg_reduce.
rewrite degM_proper.
Expand Down Expand Up @@ -411,8 +411,8 @@ rewrite polyDE; pose c := (bigi _ _ _ _); have ->: c.[k] = Coeff.zeror.
move=> i [/mem_range [ge0_i lt_in] @/predC1 ne_ik].
by rewrite polyZE polyXnE // (eq_sym k i) ne_ik /= mulr0.
rewrite addr0 polyZE polyXnE //= mulr1 (reducewE (2 * n)).
- case: (p = poly0) => [->|nz_p]; first by rewrite /( * ) mul0r deg0 /#.
case: (q = poly0) => [->|nz_q]; first by rewrite /( * ) mulr0 deg0 /#.
- case: (p = poly0) => [->|nz_p]; first by rewrite mul0r deg0 /#.
case: (q = poly0) => [->|nz_q]; first by rewrite mulr0 deg0 /#.
apply: (ler_trans (deg p + deg q)); last first.
- by rewrite (_ : 2 * n = n + n) 1:#ring ler_add &(deg_reduced).
by rewrite &(ler_trans (deg (p * q) + 1)) ?ler_addl // &(degM_le).
Expand Down
4 changes: 2 additions & 2 deletions theories/algebra/Ring.ec
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -698,7 +698,7 @@ abstract theory ComRingDflInv.

realize mulVr.
proof.
move=> x ^ un_x [y ^ -> <-] @/invr_.
move=> x ^ un_x [y ^ -> <-].
by have /= -> := choicebP _ x un_x.
qed.

Expand All @@ -707,7 +707,7 @@ abstract theory ComRingDflInv.

realize unitout.
proof.
by move=> x; rewrite /unit_ negb_exists => /choiceb_dfl /(_ x).
by move=> x; rewrite negb_exists => /choiceb_dfl /(_ x).
qed.
end ComRingDflInv.

Expand Down
2 changes: 1 addition & 1 deletion theories/crypto/assumptions/DHIES.ec
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -79,7 +79,7 @@ theory DHIES.
pkl = map (snd \o snd) kk =>
menc pkl tag ptxt = dmap (mencDHIES tag ptxt kk) (List.map (snd \o snd)).
proof.
rewrite /mencDHIES /menc /dlistmap /zipks /encDHIES /=.
rewrite /mencDHIES /menc /encDHIES /=.
rewrite djoin_dmap.
move=> ->; rewrite -map_comp /(\o) /=.
congr; congr; apply fun_ext => x.
Expand Down
2 changes: 1 addition & 1 deletion theories/distributions/DList.ec
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -326,7 +326,7 @@ rewrite -(dlet_dmap _ C (fun ds => dmap d (F ds))) -dlist_add ~-1:/#.
rewrite -(dmap_dprodE _ _ (fun (xy : _ * _) => F xy.`1 xy.`2)) /F /=.
rewrite dlistSr ~-1:/# /= !dmap_dprodE_swap /= &(in_eq_dlet) /=.
move=> x _; rewrite -(dmap_comp h (fun xs => rcons xs x)); congr.
apply: ih => @/k2; 2,3: by smt().
apply: ih; 2,3: by smt().
have ->: k1 + (n - (k1 + 1)) = n - 1 by ring.
by have := inrgf 0 _; smt().
qed.
Expand Down
6 changes: 3 additions & 3 deletions theories/distributions/Distr.ec
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2821,7 +2821,7 @@ pose F x := fun n : int => mass (df n) x.
split=> @/mdlim /= [x|s uq_s].
- case: (converge (F x))%RealSeq => [|/lim_Ncnv ->//].
apply: (geC_lim_from 0) => n _.
by rewrite /s /F massE ge0_mu1.
by rewrite /F massE ge0_mu1.
rewrite (@bigID _ _ (fun x => RealSeq.converge (F x))).
rewrite addrC big1 -1:add0r.
- by move=> x [_ @/predC] /lim_Ncnv /=; apply.
Expand Down Expand Up @@ -3411,11 +3411,11 @@ lemma Jensen_fin ['a] (d : 'a distr) f g :
=> (forall a b, convex g a b)
=> g (E d f) <= E d (g \o f).
proof.
move=> fin_d ll_d cvx_g; rewrite !fin_expE /(\o) //; pose s := to_seq _.
move=> fin_d ll_d cvx_g; rewrite !fin_expE //; pose s := to_seq _.
move: ll_d; rewrite /is_lossless weightE !(@sumE_fin _ s) ?uniq_to_seq //=.
- by move=> a; rewrite -supportP mem_to_seq.
move=> {fin_d}; case: s => [|i s]; first by rewrite BRA.big_nil.
rewrite !BRA.big_consT /=.
rewrite !BRA.big_consT /(\o) /=.
elim: s (mu1 d i) (ge0_mu d (pred1 i)) (f i) => [|x s ih] l ge0_l v.
- by rewrite !BRA.big_nil /= => ->.
rewrite !BRA.big_consT /=; have := ge0_mu d (pred1 x).
Expand Down
2 changes: 1 addition & 1 deletion theories/prelude/Logic.ec
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -692,7 +692,7 @@ proof. by move => [y fy] @/pinv; rewrite ifT; smt(choicebP). qed.

lemma pcancel_pinv (f : 'a->'b):
injective f => pcancel f (pinv f).
proof. by move => inj_f @/pcansel x; smt(pinv_inv). qed.
proof. by move => inj_f x; smt(pinv_inv). qed.


(* -------------------------------------------------------------------- *)
Expand Down
Loading