search

jasmin-lang / jasmin

Language for high-assurance and high-speed cryptography
MIT License
250 stars 53 forks source link

Missing EC keywords - toEC.ml #297

Open tfaoliveira opened 1 year ago

tfaoliveira commented 1 year ago

I had an issue with a missing keyword: the implementation used eta as a variable name, but since it is not declared in ec_keyword, EasyCrypt would print a parse error.

I took a look into EasyCrypt keywords, and I found out that some others might be missing. I attach a complete list of the keywords (in a format that I believe should be simple to c&p to toEC.ml). Since I don't know what kind of implication this has on other components, or even if the attached list is valid, I prefer to not propose the required changes myself.

keywords_jasmin.sorted.txt

(for reference, the attached list was obtained by running kw=$(cat easycrypt/src/ecLexer.mll | sed '1,/ let _keywords = \[/d;/ \]/,$d' | grep -oE "\"[a-zA-Z]*\"" | sort -u | tr '\n' ';' | sed -e 's/\;$//'); echo -e "let ec_keyword = \n [ $kw\n ]" | sed -e 's/";/"\n ; /g' ; dirty hack to get the job done quickly, but not exactly a permanent solution that might be implied by this comment)

strub commented 1 year ago

For information, you can extract the keywords with:

./scripts/srctx/keywords -m raw < src/ecLexer.mll
bgregoir commented 1 year ago

Yes, we should use this. Thank PY.