EasyCrypt / easycrypt

EasyCrypt: Computer-Aided Cryptographic Proofs
MIT License
321 stars 49 forks source link

Cannot locate jasmin theory 'JModel_x86' #446

Closed Unlimitosu closed 1 year ago

Unlimitosu commented 1 year ago

Hello, I'm now trying to execute EasyCrypt.

When I run EasyCrypt, the following error occurs:

[critical] [: line 1 (0) to line 2 (38)] cannot locate theory `JModel_x86'
[/] [0003] 1.5% (-1.0B / [frag -1.0B])

I thought it's because of configuring jasminc path to easycrypt.conf. So, I added includepath=/usr/local/bin/jasminc to easycrypt.conf but same error occured.

I tried also includepath=[/usr/local/bin/jasminc], but it didn't work.

Here is a EasyCrypt Code which I extracted from Jasmin:

require import AllCore IntDiv CoreMap List Distr.
from Jasmin require import JModel_x86.
import SLH64.

from Jasmin require import JLeakage.
require import Array128.
require import WArray512.

What's wrong with me? and how can I solve this issue?

vbgl commented 1 year ago

Related: https://github.com/jasmin-lang/jasmin/wiki/Extraction-to-EasyCrypt#configure-easycrypt-to-verify-jasmin-programs

Unlimitosu commented 1 year ago

oh I didn't know what does the path mean. Now it works. Thanks