running failed at examples/MEE-CBC

[liuty-liuty]

I run easycrypt on Ubuntu 20.04 LTS with ocaml-base-compiler.4.10.0, alt-ergo with version 2.4.2 and 2.4.3, there seems no problem with dependencies.

elgamal.ec in example could output a result:

.../easycrypt-main/easycrypt-main/examples$ easycrypt elgamal.ec
* In [lemmas or axioms]: / [frag -1.0B])

lemma conclusion:
  forall (A <: Adversary),
    islossless A.choose =>
    islossless A.guess =>
    forall &m,
      `|Pr[CPA(ElGamal, A).main() @ &m : res] - 1%r / 2%r| =
      `|Pr[DDH0(DDHAdv(A)).main() @ &m : res] -
        Pr[DDH1(DDHAdv(A)).main() @ &m : res]|.

While when I test FunctionalSpec in MEE-CBC, there comes mistakes:

.../easycrypt-main/examples/MEE-CBC$ easycrypt FunctionalSpec.ec
[warning] [FunctionalSpec.ec:299] prover Alt-Ergo exited with High failure
[warning] [FunctionalSpec.ec:299] prover Alt-Ergo exited with High failure
[warning] [FunctionalSpec.ec:299] prover Alt-Ergo exited with High failure
[warning] [FunctionalSpec.ec:299] prover Alt-Ergo exited with High failure
[warning] [FunctionalSpec.ec:299] prover Alt-Ergo exited with High failure
[warning] [FunctionalSpec.ec:299] prover Alt-Ergo exited with High failure
[critical] [FunctionalSpec.ec: line 299 (42-64)] cannot prove goal (strict)
[-] [0299] 51.2% (-1.0B / [frag -1.0B])

also does not work with _RCPACMA.ec:

...easycrypt-main/examples/MEE-CBC$ easycrypt RCPA_CMA.ec
[warning] [RCPA_CMA.ec:27] prover Alt-Ergo exited with High failure
[warning] [RCPA_CMA.ec:27] prover Alt-Ergo exited with High failure
[warning] [RCPA_CMA.ec:27] prover Alt-Ergo exited with High failure
[warning] [RCPA_CMA.ec:27] prover Alt-Ergo exited with High failure
[warning] [RCPA_CMA.ec:27] prover Alt-Ergo exited with High failure
[warning] [RCPA_CMA.ec:27] prover Alt-Ergo exited with High failure
[critical] [: line 1 (0) to line 26 (17)] In proving `dC_ll':

cannot prove goal (strict)

Initial goal was:

Type variables: <none>

------------------------------------------------------------------------
forall (p : leaks), is_lossless (dC p)
[-] [0027] 4.2% (-1.0B / [frag -1.0B])

When I tried to use z3, there still no correct results:

.../easycrypt-main/examples/MEE-CBC$ easycrypt RCPA_CMA.ec
[critical] [: line 1 (0) to line 259 (23)] cannot prove goal (strict)
[\] [0260] 39.1% (-1.0B / [frag -1.0B])

.../easycrypt-main/examples/MEE-CBC$ easycrypt FunctionalSpec.ec
[critical] [FunctionalSpec.ec: line 326 (50-63)] cannot prove goal (strict)
[|] [0326] 56.3% (-1.0B / [frag -1.0B])

So..could someone help me to fix the problem?

[fdupress]

Some of the examples require multiple provers to be set up and runnable at the same time to check. (That is, some goals will be dispatched by Z3, and others by Alt-Ergo.) We recommend a minimum of Alt-Ergo (2.4.2 if possible), Z3 and CVC4, who have complementary strengths.

[liuty-liuty]

Thanks for your reply, while problem still unsolved..

The warning below report could not find why3.conf, while it actually exist.

Executing: why3 config detect -C /home/liuty/.config/easycrypt/why3.conf warning: cannot read config file /home/liuty/.config/easycrypt/why3.conf: /home/liuty/.config/easycrypt/why3.conf: No such file or directory

Prove failed with Z3 and CVC4:

.../easycrypt-main/examples/MEE-CBC$ easycrypt why3config
Executing: why3 config detect -C /home/liuty/.config/easycrypt/why3.conf
warning: cannot read config file /home/liuty/.config/easycrypt/why3.conf:
  /home/liuty/.config/easycrypt/why3.conf: No such file or directory
Found prover CVC4 version 1.8 (alternative: strings+counterexamples)
Found prover CVC4 version 1.8 (alternative: strings)
Found prover CVC4 version 1.8 (alternative: counterexamples)
Found prover CVC4 version 1.8, OK.
Found prover Z3 version 4.12.2 (alternative: counterexamples)
Found prover Z3 version 4.12.2, OK.
Found prover Z3 version 4.12.2 (alternative: noBV)
7 prover(s) added
Save config to /home/liuty/.config/easycrypt/why3.conf
.../easycrypt-main/examples/MEE-CBC$ easycrypt FunctionalSpec.ec
[critical] [FunctionalSpec.ec: line 333 (44-57)] cannot prove goal (strict)
[-] [0334] 57.4% (-1.0B / [frag -1.0B])

Prove failed with Alt-Ergo 2.4.2(2.4.3), CVC4 and Z3:

.../easycrypt-main/examples/MEE-CBC$ easycrypt why3config
Executing: why3 config detect -C /home/liuty/.config/easycrypt/why3.conf
warning: cannot read config file /home/liuty/.config/easycrypt/why3.conf:
  /home/liuty/.config/easycrypt/why3.conf: No such file or directory
Found prover Alt-Ergo version 2.4.2, OK.
Found prover Alt-Ergo version 2.4.2 (alternative: FPA)
Found prover CVC4 version 1.8 (alternative: strings+counterexamples)
Found prover CVC4 version 1.8 (alternative: strings)
Found prover CVC4 version 1.8 (alternative: counterexamples)
Found prover CVC4 version 1.8, OK.
Found prover Z3 version 4.12.2 (alternative: counterexamples)
Found prover Z3 version 4.12.2, OK.
Found prover Z3 version 4.12.2 (alternative: noBV)
9 prover(s) added
Save config to /home/liuty/.config/easycrypt/why3.conf
.../easycrypt-main/examples/MEE-CBC$ easycrypt FunctionalSpec.ec
[warning] [FunctionalSpec.ec:326] prover Alt-Ergo exited with High failure
[warning] [FunctionalSpec.ec:334] prover Alt-Ergo exited with High failure
[warning] [FunctionalSpec.ec:334] prover Alt-Ergo exited with High failure
[warning] [FunctionalSpec.ec:334] prover Alt-Ergo exited with High failure
[warning] [FunctionalSpec.ec:334] prover Alt-Ergo exited with High failure
[warning] [FunctionalSpec.ec:334] prover Alt-Ergo exited with High failure
[warning] [FunctionalSpec.ec:334] prover Alt-Ergo exited with High failure
[critical] [FunctionalSpec.ec: line 333 (44-57)] cannot prove goal (strict)
[/] [0334] 57.4% (-1.0B / [frag -1.0B])

[strub]

The warning (which comes from Why3) tells you that the file does not initially exist. However, once the command is over, you should see a file named /home/liuty/.config/easycrypt/why3.conf

[liuty-liuty]

The goal of these examples still cannot be proved, though the reply > The warning (which comes from Why3) tells you that the file does not initially exist. However, once the command is over, you should see a file named /home/liuty/.config/easycrypt/why3.conf is reasonable.

Further, the failure of proof (run easycrypt examples/...) seem consist with these failures below (run make ...).

run make check at the root of the EasyCrypt source tree, output 38 failures:

⁕ [ 8:13] Success: 81, Failure: 34, Running: 4, Waiting: 0
▶ [ϟ] theories/structure/Finite.ec
⁕ [ 8:23] Success: 81, Failure: 34, Running: 4, Waiting: 0
      theories/structure/Finite.ec:67 prover Alt-Ergo exited with High failure
⁕ [ 8:23] Success: 81, Failure: 34, Running: 4, Waiting: 0
▶ [✗] theories/crypto/prp_prf/Strong_RP_RF.eca
⁕ [ 8:24] Success: 81, Failure: 34, Running: 4, Waiting: 0
      : line 1 (0) to line 147 (38) cannot prove goal (strict)
⁕ [ 8:24] Success: 81, Failure: 34, Running: 4, Waiting: 0
▶ [✗] [ 1:53.8] theories/crypto/prp_prf/Strong_RP_RF.eca
⁕ [ 8:24] Success: 81, Failure: 34, Running: 4, Waiting: 0
▶ [ϟ] theories/crypto/assumptions/DHIES.ec
      theories/crypto/assumptions/DHIES.ec:260 prover Alt-Ergo exited with High failure
▶ [ϟ] theories/datatypes/List.ec
      theories/datatypes/List.ec:310 prover Alt-Ergo exited with High failure
▶ [✗] theories/crypto/assumptions/DHIES.ec
      : line 1 (0) to line 259 (47) cannot prove goal (strict)
▶ [✗] [ 2:38.5] theories/crypto/assumptions/DHIES.ec
▶ [ϟ] theories/structure/Finite.ec
      theories/structure/Finite.ec:67 prover Alt-Ergo exited with High failure
▶ [✗] theories/datatypes/List.ec
      : line 1 (0) to line 310 (32) cannot prove goal (strict)
▶ [✗] [ 6:02.8] theories/datatypes/List.ec
▶ [✗] theories/structure/Finite.ec
      theories/structure/Finite.ec: line 66 (45-46) cannot prove goal (strict)
▶ [✗] [ 3:57.8] theories/structure/Finite.ec
⁕ [ 9:41] Success: 81, Failure: 38, Running: 0, Waiting: 0
make: *** [Makefile:44: stdlib] Error 2

run make examples at the root of the EasyCrypt source tree, output 12 failures:

...
...
   : line 1 (0) to line 795 (74) cannot prove goal (strict)
▶ [✗] [ 3:01.1] examples/ChaChaPoly/chacha_poly.ec
▶ [ϟ] examples/cramer-shoup/cramer_shoup.ec
      examples/cramer-shoup/cramer_shoup.ec:873 prover Alt-Ergo exited with High failure
▶ [✗] examples/UC/composition_cost.ec
      examples/UC/composition_cost.ec: line 895 (43-44) cannot prove goal (strict)
▶ [✗] [ 2:44.9] examples/UC/composition_cost.ec
▶ [ϟ] examples/MEE-CBC/CBC.eca
      examples/MEE-CBC/CBC.eca:509 prover Alt-Ergo exited with High failure
▶ [✗] examples/cramer-shoup/cramer_shoup.ec
      : line 1 (0) to line 872 (43) cannot prove goal (strict)
▶ [✗] [ 3:03.0] examples/cramer-shoup/cramer_shoup.ec
▶ [✗] examples/MEE-CBC/CBC.eca
      : line 1 (0) to line 509 (52) cannot prove goal (strict)
▶ [✗] [ 2:55.5] examples/MEE-CBC/CBC.eca
⁕ [ 3:24] Success: 28, Failure: 12, Running: 0, Waiting: 0
make: *** [Makefile:47: examples] Error 2

Is there some setting neglected like Path?

.../easycrypt-main/examples/MEE-CBC$ easycrypt config
git-hash: n/a
load-path:
  <system>@/home/liuty/.opam/easycrypt/bin/../lib/easycrypt/theories
  <system>@/home/liuty/.opam/easycrypt/bin/../lib/easycrypt/theories/tactics
  <system>@/home/liuty/.opam/easycrypt/bin/../lib/easycrypt/theories/structure
  <system>@/home/liuty/.opam/easycrypt/bin/../lib/easycrypt/theories/query_counting
  <system>@/home/liuty/.opam/easycrypt/bin/../lib/easycrypt/theories/newth
  <system>@/home/liuty/.opam/easycrypt/bin/../lib/easycrypt/theories/modules
  <system>@/home/liuty/.opam/easycrypt/bin/../lib/easycrypt/theories/looping
  <system>@/home/liuty/.opam/easycrypt/bin/../lib/easycrypt/theories/encryption
  <system>@/home/liuty/.opam/easycrypt/bin/../lib/easycrypt/theories/distributions
  <system>@/home/liuty/.opam/easycrypt/bin/../lib/easycrypt/theories/datatypes
  <system>@/home/liuty/.opam/easycrypt/bin/../lib/easycrypt/theories/crypto
  <system>@/home/liuty/.opam/easycrypt/bin/../lib/easycrypt/theories/crypto/ske
  <system>@/home/liuty/.opam/easycrypt/bin/../lib/easycrypt/theories/crypto/prp_prf
  <system>@/home/liuty/.opam/easycrypt/bin/../lib/easycrypt/theories/crypto/pke
  <system>@/home/liuty/.opam/easycrypt/bin/../lib/easycrypt/theories/crypto/assumptions
  <system>@/home/liuty/.opam/easycrypt/bin/../lib/easycrypt/theories/core
  <system>@/home/liuty/.opam/easycrypt/bin/../lib/easycrypt/theories/analysis
  <system>@/home/liuty/.opam/easycrypt/bin/../lib/easycrypt/theories/algebra
  <system>@/home/liuty/.opam/easycrypt/bin/../lib/easycrypt/theories/prelude
why3 configuration file
  /home/liuty/.config/easycrypt/why3.conf
EasyCrypt configuration file
  <none>
known provers: Z3@4.12.2, Z3@4.12.2, Z3@4.12.2, CVC4@1.8, CVC4@1.8, CVC4@1.8, CVC4@1.8, Alt-Ergo@2.4.3, Alt-Ergo@2.4.3
System PATH:
  /home/liuty/.opam/easycrypt/bin
  /usr/local/bin
  /usr/bin
  /bin

[fdupress]

Can you please try the following: a. Install z3 4.8.10 (or set it up before your system-wide install in PATH, downloading the release from GitHub; you only need the binary in your PATH); b. Run easycrypt why3config again (and check that z3 4.8.10 gets selected); c. Try running make check again?

Can you please also confirm which easycrypt version/branch/git hash you are using? I would have expected it to show in the output of easycrypt config even with a make check.

[fdupress]

Wait. make check would use a locally compiled version of easycrypt, but the output of easycrypt config is from an opam switch that should definitely have a commit hash set. How did you install easycrypt via opam?

[liuty-liuty]

There seems no z3 4.8.10, so I used z3 4.12.2.

I have tried several easycrypt versions, the recently I used is installed with command opam install easycrypt. And I also tried make , make installfrom the recently easycrypt-main.

The compiler I used is ocaml-base-compiler.5.0.0, other versions of ocaml-base-compiler(4.08.1) seems not success with me.

[liuty-liuty]

The main purpose of me is learning to run an example with local library(.eca), like examples/MEE-CBC. Something wrong as we are discussing.

[chdoc]

The compiler I used is ocaml-base-compiler.5.0.0, other versions of ocaml-base-compiler(4.08.1) seems not success with me.

There are known issues with ocaml-5.0 You may want to try a more recent 4.x compiler (4.11.2 works for me)

That being said, my set up also cannot (reliably) check every single example. I am using:

known provers: Z3@4.8.17, Z3@4.8.17, Z3@4.8.17, Isabelle@2022, CVC4@1.8, CVC4@1.8, CVC4@1.8, CVC4@1.8, Alt-Ergo@2.4.2, Alt-Ergo@2.4.2

Also, make check is very parallel by default, and this may cause issues. You may want to try ECRJOBS=1 make check, disabling parallel checking of files. If your computer is older/slower, you may also increase the smt timeout, e.g. by setting ECTOUT=30

[liuty-liuty]

Thanks for your reply. One operation system on-line I used is available for most of these examples, while a shortage is that I need to configure it every time I use.

And I have further questions: a. Some of examples could run haven't any output, only with a file with(.eco). I hardly know what it represents. b. Have you ever met [critical] ... unknown predicate 'p', some of .ec files have such errors.

[chdoc]

Some of examples could run haven't any output, only with a file with(.eco). I hardly know what it represents.

Generally, if a file checks correctly there shouldn't be any output printed. You should look inside the file to see which lemmas have been stated/proved.

Have you ever met [critical] ... unknown predicate 'p', some of .ec files have such errors.

This is most likely due to the file you're trying to check not having been updated to the recent changes in the SubType theory. If you encounter this while trying to check files from the EasyCrypt distribution, this probably means you are (accidentally) mixing filed from different versions of the library.

[oskgo]

I had a similar problem with smt solver configuration recently, which I solved by setting the environment variable XDG_CONFIG_HOME to an appropriate value (where your os distribution wants your config files to be) and then running easycrypt why3config.

[liuty-liuty]

@chdoc @oskgo sorry for the late reply, your suggestions are helpful to me:)

[fdupress]

I'll close this now, since it looks like the discussion is less active.