Encryption_2W.v doesn't build

adampetcher / fcf

Foundational Cryptography Framework for machine-checked proofs of cryptography.

Other

48 stars 23 forks source link

Encryption_2W.v doesn't build #5

Closed asya-bergal closed 7 years ago

asya-bergal commented 7 years ago

I was trying to use IND_CPA_SecretKey_equiv from Encryption_2W.v, but building Encryption_2W.v seems to fail on the line: Context{EncryptionScheme_SecretKey}`.

I couldn't find EncryptionScheme_SecretKey in the file directory or the Git commit history. Looks like it was never committed? What would need to be done to get this file to compile?

adampetcher commented 7 years ago

I pulled in a PR from Andres that got TwoWorldsEquiv working again. If I remember correctly, this is a more general form of the argument in Encryption_2W, so it should work for your purposes. Can you confirm that this is the case? If so, we should probably just remove Encryption_2W.

adampetcher commented 7 years ago

This file has been moved to the Broken directory, so I will deal with it in issue #12.