Adding a top-level comment to one of the Coq files.

apetcher-amazon · Apr 10, 2024 · b5bb507 · b5bb507
1 parent d9cb16d
commit b5bb507
Showing 1 changed file with 3 additions and 0 deletions.
diff --git a/Coq/EC/EC_P384_Abstract_5_equiv.v b/Coq/EC/EC_P384_Abstract_5_equiv.v
@@ -1,6 +1,9 @@
 (* Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
 SPDX-License-Identifier: Apache-2.0 *)
 
+(* Proof of equivalence between the spec extracted from Cryptol and the hand-written
+low-level specification in EC_P384_Abstract. *)
+
 Set Implicit Arguments.
 
 From Coq Require Import Lists.List.