rewrite lemmas with Exponents (Big Numbers)

[henriquejosefaria]

When rewriting a lemma with exponents it takes a long time to finish. The problem occurs both in rewrite bound and rewrite (ltz_trans ....).

require import AllCore IntDiv.

op p1:int.
op base: int.
op exp1: int.

axiom base_ge0:0 <= base.
axiom exp1_gt0:0 < exp1.
axiom prime_p1: prime p1.
axiom bound: p1 < 2^2048.

lemma supper_slow:
0 <= base ^ exp1 %% p1 && base ^ exp1 %% p1 < 2^2048.
proof.
  have H0: p1 < 2^2048 by rewrite bound.
  pose m := base ^ exp1 %% p1.
  have H1: m < p1. rewrite /m ltz_pmod (ltz_trans 1 0 p1) 1:/#. smt(prime_p1).
  rewrite (ltz_trans p1 m (2^2048) H1 H0).
  rewrite modz_ge0. print gt0_prime.
  have aux: 0 < p1 by rewrite (gt0_prime p1 prime_p1) /#.
  smt(). smt().
qed.

[strub]

Hi. I cannot reproduce. Which version of EasyCrypt are you using?

[henriquejosefaria]

The version I'm working with is the last verified commit: https://github.com/EasyCrypt/easycrypt/tree/791bfa740a20f7ebf346edb2ba2836b63b8d340d

[strub]

I cannot reproduce with the commit you gave. Do you confirm that the snippet above exhibits the behavior on your side?

[fdupress]

Could it be an ocaml version/memory explosion issue?

[strub]

Could it be an ocaml version/memory explosion issue?

soupir. Indeed, I missed that. So, @henriquejosefaria, which version of OCaml are you using?

[henriquejosefaria]

OCaml version 4.14.1

[strub]

I confirm that I cannot reproduce the bug.

[fdupress]

Also could not reproduce on Linux, neither on CLI nor in PG. Henrique, I think we still need to know if the exact snippet above, when run in isolation, exhibits the unexpected slowness for you.

And if so, I guess we'll need to dive into details of your platform so we can try to reproduce.

[strub]

@henriquejosefaria ?

[henriquejosefaria]

First, I need to say it seems to me the lengthier the proof, the slower the performance on ltz_trans. Currently, I am using a Mackbook pro with a 2,3 GHz Quad-Core Intel Core i7, and the macOS version is Sonoma 14.6.1.