Merge pull request #13 from shigoel/copyright_header

Add LICENSE info. in the file copyright headers
leanprover · Feb 15, 2024 · df583d7 · df583d7
2 parents 8184ccf + 43a5a4e
commit df583d7
Show file tree

Hide file tree

Showing 65 changed files with 66 additions and 1 deletion.
diff --git a/Arm.lean b/Arm.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel
 -/
 -- This module serves as the root of the `Arm` library.

diff --git a/Arm/BitVec.lean b/Arm/BitVec.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel
 -/
 

diff --git a/Arm/Cfg/Cfg.lean b/Arm/Cfg/Cfg.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel
 -/
 import Arm.Exec

diff --git a/Arm/Cosim.lean b/Arm/Cosim.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel
 -/
 import Arm.Exec

diff --git a/Arm/Decode.lean b/Arm/Decode.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel
 -/
 import Arm.Memory

diff --git a/Arm/Decode/BR.lean b/Arm/Decode/BR.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel, Yan Peng
 -/
 import Arm.BitVec

diff --git a/Arm/Decode/DPI.lean b/Arm/Decode/DPI.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel
 -/
 import Arm.BitVec

diff --git a/Arm/Decode/DPR.lean b/Arm/Decode/DPR.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel, Yan Peng
 -/
 import Arm.BitVec

diff --git a/Arm/Decode/DPSFP.lean b/Arm/Decode/DPSFP.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel
 -/
 import Arm.BitVec

diff --git a/Arm/Decode/LDST.lean b/Arm/Decode/LDST.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel
 -/
 import Arm.BitVec

diff --git a/Arm/Exec.lean b/Arm/Exec.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel
 -/
 import Arm.BitVec

diff --git a/Arm/Insts.lean b/Arm/Insts.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel
 -/
 import Arm.Insts.DPI.Insts

diff --git a/Arm/Insts/BR/Compare_branch.lean b/Arm/Insts/BR/Compare_branch.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel
 -/
 

diff --git a/Arm/Insts/BR/Cond_branch_imm.lean b/Arm/Insts/BR/Cond_branch_imm.lean
@@ -1,5 +1,6 @@
-/-+
+/-
 Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Yan Peng
 -/
 

diff --git a/Arm/Insts/BR/Insts.lean b/Arm/Insts/BR/Insts.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel
 -/
 import Arm.Insts.BR.Compare_branch

diff --git a/Arm/Insts/BR/Uncond_branch_imm.lean b/Arm/Insts/BR/Uncond_branch_imm.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel
 -/
 

diff --git a/Arm/Insts/BR/Uncond_branch_reg.lean b/Arm/Insts/BR/Uncond_branch_reg.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel
 -/
 

diff --git a/Arm/Insts/Common.lean b/Arm/Insts/Common.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel, Yan Peng
 -/
 import Arm.BitVec

diff --git a/Arm/Insts/Cosim/disasm.sh b/Arm/Insts/Cosim/disasm.sh
@@ -1,4 +1,5 @@
 # Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+# Released under Apache 2.0 license as described in the file LICENSE.
 # Author(s): Shilpi Goel
 
 #!/bin/sh

diff --git a/Arm/Insts/Cosim/platform_check.sh b/Arm/Insts/Cosim/platform_check.sh
@@ -1,4 +1,5 @@
 # Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+# Released under Apache 2.0 license as described in the file LICENSE.
 # Author(s): Shilpi Goel
 
 #!/bin/bash

diff --git a/Arm/Insts/DPI/Add_sub_imm.lean b/Arm/Insts/DPI/Add_sub_imm.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel
 -/
 -- ADD, ADDS, SUB, SUBS (immediate): 32- and 64-bit versions

diff --git a/Arm/Insts/DPI/Insts.lean b/Arm/Insts/DPI/Insts.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel
 -/
 import Arm.Insts.DPI.Add_sub_imm

diff --git a/Arm/Insts/DPI/Logical_imm.lean b/Arm/Insts/DPI/Logical_imm.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Yan Peng
 -/
 -- AND, ORR, EOR, ANDS (immediate): 32- and 64-bit versions

diff --git a/Arm/Insts/DPI/PC_rel_addressing.lean b/Arm/Insts/DPI/PC_rel_addressing.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel
 -/
 -- ADR, ADRP

diff --git a/Arm/Insts/DPR/Add_sub_carry.lean b/Arm/Insts/DPR/Add_sub_carry.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel
 -/
 -- ADC, ADCS, SBC, SBCS: 32- and 64-bit versions

diff --git a/Arm/Insts/DPR/Add_sub_shifted_reg.lean b/Arm/Insts/DPR/Add_sub_shifted_reg.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Yan Peng
 -/
 -- ADD, ADDS, SUB, SUBS (shifted registers): 32- and 64-bit versions

diff --git a/Arm/Insts/DPR/Conditional_select.lean b/Arm/Insts/DPR/Conditional_select.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel
 -/
 -- CSEL, CSINC, CSINV, CSNEG: 32- and 64-bit versions

diff --git a/Arm/Insts/DPR/Insts.lean b/Arm/Insts/DPR/Insts.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel
 -/
 import Arm.Insts.DPR.Add_sub_carry

diff --git a/Arm/Insts/DPR/Logical_shifted_reg.lean b/Arm/Insts/DPR/Logical_shifted_reg.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Yan Peng
 -/
 -- AND, BIC, ORR, ORN, EOR, EON, ANDS, BICS: 32- and 64-bit versions

diff --git a/Arm/Insts/DPSFP/Advanced_simd_extract.lean b/Arm/Insts/DPSFP/Advanced_simd_extract.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel
 -/
 -- EXT

diff --git a/Arm/Insts/DPSFP/Advanced_simd_three_same.lean b/Arm/Insts/DPSFP/Advanced_simd_three_same.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel, Yan Peng
 -/
 -- ADD, ORR, AND, BIC, ORR, ORN, EOR, BSL, BIT, BIF (vector)

diff --git a/Arm/Insts/DPSFP/Advanced_simd_two_reg_misc.lean b/Arm/Insts/DPSFP/Advanced_simd_two_reg_misc.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel
 -/
 -- REV64

diff --git a/Arm/Insts/DPSFP/Crypto_aes.lean b/Arm/Insts/DPSFP/Crypto_aes.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel
 -/
 -- AESE, AESMC

diff --git a/Arm/Insts/DPSFP/Crypto_three_reg_sha512.lean b/Arm/Insts/DPSFP/Crypto_three_reg_sha512.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel
 -/
 -- SHA512H, SHA512H2, SHA512SU1

diff --git a/Arm/Insts/DPSFP/Crypto_two_reg_sha512.lean b/Arm/Insts/DPSFP/Crypto_two_reg_sha512.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel
 -/
 -- SHA512SU0

diff --git a/Arm/Insts/DPSFP/Insts.lean b/Arm/Insts/DPSFP/Insts.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel
 -/
 import Arm.Insts.DPSFP.Advanced_simd_two_reg_misc

diff --git a/Arm/Insts/LDST/Advanced_simd_multiple_struct.lean b/Arm/Insts/LDST/Advanced_simd_multiple_struct.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel
 -/
 -- LDP, STP

diff --git a/Arm/Insts/LDST/Insts.lean b/Arm/Insts/LDST/Insts.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel
 -/
 import Arm.Insts.LDST.Reg_imm

diff --git a/Arm/Insts/LDST/Reg_imm.lean b/Arm/Insts/LDST/Reg_imm.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel
 -/
 -- LDR/STR (immediate, SIMD&FP)

diff --git a/Arm/Insts/LDST/Reg_pair.lean b/Arm/Insts/LDST/Reg_pair.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel
 -/
 -- LDP, STP

diff --git a/Arm/Memory.lean b/Arm/Memory.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel
 -/
 import Arm.Separate

diff --git a/Arm/MemoryProofs.lean b/Arm/MemoryProofs.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel
 -/
 import Arm.SeparateProofs

diff --git a/Arm/Separate.lean b/Arm/Separate.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel
 -/
 import Arm.State

diff --git a/Arm/SeparateProofs.lean b/Arm/SeparateProofs.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel
 -/
 import Arm.Memory

diff --git a/Arm/State.lean b/Arm/State.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel
 -/
 import Arm.BitVec

diff --git a/Main.lean b/Main.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel
 -/
 import «Arm»

diff --git a/Makefile b/Makefile
@@ -1,4 +1,5 @@
 # Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+# Released under Apache 2.0 license as described in the file LICENSE.
 # Author(s): Shilpi Goel
 
 SHELL := /bin/bash

diff --git a/Proofs.lean b/Proofs.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel
 -/
 -- This module serves as the root of the `Proofs` library.

diff --git a/Proofs/MultiInsts.lean b/Proofs/MultiInsts.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel
 -/
 import Arm.Exec

diff --git a/Proofs/Proofs.lean b/Proofs/Proofs.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel
 -/
 import «Proofs».MultiInsts

diff --git a/Proofs/SHA512_AssocRepr.lean b/Proofs/SHA512_AssocRepr.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel
 -/
 import Arm.Exec

diff --git a/Proofs/Sha512_block_armv8.lean b/Proofs/Sha512_block_armv8.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel
 -/
 import Arm.Exec

diff --git a/Proofs/Sha512_block_armv8_rules.lean b/Proofs/Sha512_block_armv8_rules.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel
 -/
 import Arm.Insts.DPSFP.Insts

diff --git a/Proofs/Test.lean b/Proofs/Test.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel
 -/
 import Arm.Exec

diff --git a/Specs/AESCommon.lean b/Specs/AESCommon.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel
 -/
 import Arm.BitVec

diff --git a/Specs/SHA512.lean b/Specs/SHA512.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel, Yan Peng
 -/
 import Std.Data.BitVec

diff --git a/Specs/SHA512Common.lean b/Specs/SHA512Common.lean
@@ -1,5 +1,6 @@
 /-
 Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Shilpi Goel
 -/
 import Arm.BitVec