From 6b9af159ff5c77149d3aee709f106c19f6b39cca Mon Sep 17 00:00:00 2001 From: Manuel Barbosa Date: Wed, 27 Nov 2024 19:13:11 +0000 Subject: [PATCH] pending --- easycrypt.project | 2 -- proof/security/MLWE_PKE.ec | 2 +- 2 files changed, 1 insertion(+), 3 deletions(-) diff --git a/easycrypt.project b/easycrypt.project index 7123e044..842092c4 100644 --- a/easycrypt.project +++ b/easycrypt.project @@ -6,11 +6,9 @@ provers = CVC4@1.8 provers = Z3@4.8 rdirs = proof -rdirs = ../easycrypt/examples rdirs = Jasmin:jasmin/eclib idirs = code/jasmin/mlkem_ref/extraction idirs = code/jasmin/mlkem_avx2/extraction idirs = crypto-specs/common rdirs = crypto-specs/fips202 rdirs = crypto-specs/ml-kem -rdirs = ~/Desktop/Repos/easycrypt/examples diff --git a/proof/security/MLWE_PKE.ec b/proof/security/MLWE_PKE.ec index 5967406f..40fbd3c0 100644 --- a/proof/security/MLWE_PKE.ec +++ b/proof/security/MLWE_PKE.ec @@ -1,4 +1,4 @@ -require import AllCore Distr List SmtMap Dexcepted PKE_ROM. +require import AllCore Distr List FMap Dexcepted PKE_ROM. require (****) RndExcept StdOrder MLWE. theory MLWE_PKE.