add copyright banner

README.md

@@ -1,24 +1,23 @@
-# alive_in_lean
+# AliveInLean
 
 ## Setup
 
-- Please download Nighty Windows from https://leanprover.github.io/download/
+- Download Lean 3.4.1 or later from https://leanprover.github.io/download/
 - Extract it, and update PATH environmental variable so command `lean` can be executed on the command prompt
 - Download & install z3 from https://github.com/Z3Prover/z3 and update PATH so `z3` can be executed as well
 - Run `leanpkg upgrade` to install SMT lib interface and mathlib
-- NOTE: `leanpkg build` may fail, due to several yet incomplete files in submodules
 
 
 ## Run
 
 ```
-# Runs selected tests from Alive's test suite (which contain
+# Run selected tests from Alive's test suite (which contain
 # no precondition and do not require additional grammars)
 ./run-alive.sh
 ```
 
 ```
-# Runs random testings for specification of Z3 expression -
+# Run random tests for the specification of Z3 expression -
 # concrete value, as well as 4 admitted arithmetic lemmas.
 # Note that bv_equiv.zext/sext/trunc will have 'omitted' tests
 # because sometimes generated expressions try to compare

src/bitvector.lean

@@ -1,3 +1,6 @@
+-- Copyright (c) Microsoft Corporation. All rights reserved.
+-- Licensed under the MIT license.
+
 import .common
 import .ops
 

src/common.lean

@@ -1,3 +1,6 @@
+-- Copyright (c) Microsoft Corporation. All rights reserved.
+-- Licensed under the MIT license.
+
 def size := { n:nat // 0 < n }
 
 namespace size

src/freevar.lean

@@ -1,3 +1,6 @@
+-- Copyright (c) Microsoft Corporation. All rights reserved.
+-- Licensed under the MIT license.
+
 import .lang
 import .irsem
 import .irsem_exec

src/irsem.lean

@@ -1,3 +1,6 @@
+-- Copyright (c) Microsoft Corporation. All rights reserved.
+-- Licensed under the MIT license.
+
 /-
 Semantics of LLVM IR
 -/

src/irsem_exec.lean

@@ -1,3 +1,6 @@
+-- Copyright (c) Microsoft Corporation. All rights reserved.
+-- Licensed under the MIT license.
+
 import system.io
 import smt2.syntax
 import .irsem

src/irsem_smt.lean

@@ -1,3 +1,6 @@
+-- Copyright (c) Microsoft Corporation. All rights reserved.
+-- Licensed under the MIT license.
+
 import system.io
 import smt2.syntax
 import smt2.builder

src/irtype.lean

@@ -1,3 +1,6 @@
+-- Copyright (c) Microsoft Corporation. All rights reserved.
+-- Licensed under the MIT license.
+
 import .lang
 
 -- Returns true if program p contains uninstantiated type.

src/lang.lean

@@ -1,3 +1,6 @@
+-- Copyright (c) Microsoft Corporation. All rights reserved.
+-- Licensed under the MIT license.
+
 -- constant value
 inductive const : Type
 | int : ℤ → const

src/lang_tostr.lean

@@ -1,3 +1,6 @@
+-- Copyright (c) Microsoft Corporation. All rights reserved.
+-- Licensed under the MIT license.
+
 import .lang
 
 namespace const

src/langparser.lean

@@ -1,3 +1,6 @@
+-- Copyright (c) Microsoft Corporation. All rights reserved.
+-- Licensed under the MIT license.
+
 import .lang
 import .lang_tostr
 import data.buffer.parser

src/main.lean

@@ -1,3 +1,6 @@
+-- Copyright (c) Microsoft Corporation. All rights reserved.
+-- Licensed under the MIT license.
+
 import system.io
 import system.random
 import .freevar

src/ops.lean

@@ -1,3 +1,6 @@
+-- Copyright (c) Microsoft Corporation. All rights reserved.
+-- Licensed under the MIT license.
+
 import .common
 
 universes u v

src/proptest.lean

@@ -1,3 +1,6 @@
+-- Copyright (c) Microsoft Corporation. All rights reserved.
+-- Licensed under the MIT license.
+
 import system.io
 import .smtexpr
 import .smtcompile

src/proptest_run.lean

@@ -1,3 +1,5 @@
+-- Copyright (c) Microsoft Corporation. All rights reserved.
+-- Licensed under the MIT license.
 
 import system.io
 import .smtexpr

src/smtcompile.lean

@@ -1,3 +1,6 @@
+-- Copyright (c) Microsoft Corporation. All rights reserved.
+-- Licensed under the MIT license.
+
 import .smtexpr
 import smt2.syntax
 import smt2.builder

src/smtexpr.lean

@@ -1,3 +1,6 @@
+-- Copyright (c) Microsoft Corporation. All rights reserved.
+-- Licensed under the MIT license.
+
 import .common
 import .ops
 import .bitvector

src/spec/closed.lean

@@ -1,3 +1,6 @@
+-- Copyright (c) Microsoft Corporation. All rights reserved.
+-- Licensed under the MIT license.
+
 import ..smtexpr
 import ..bitvector
 import .spec

src/spec/equiv.lean

@@ -1,3 +1,6 @@
+-- Copyright (c) Microsoft Corporation. All rights reserved.
+-- Licensed under the MIT license.
+
 import ..smtexpr
 import ..smtcompile
 import ..bitvector

src/spec/freevar.lean

@@ -1,3 +1,6 @@
+-- Copyright (c) Microsoft Corporation. All rights reserved.
+-- Licensed under the MIT license.
+
 import ..smtexpr
 import ..bitvector
 import ..irsem

src/spec/initialstate.lean

@@ -1,3 +1,6 @@
+-- Copyright (c) Microsoft Corporation. All rights reserved.
+-- Licensed under the MIT license.
+
 import ..smtexpr
 import ..smtcompile
 import ..bitvector

src/spec/irstate.lean

@@ -1,3 +1,6 @@
+-- Copyright (c) Microsoft Corporation. All rights reserved.
+-- Licensed under the MIT license.
+
 import .spec
 import .lemmas
 import ..irsem

src/spec/lemmas.lean

@@ -1,3 +1,6 @@
+-- Copyright (c) Microsoft Corporation. All rights reserved.
+-- Licensed under the MIT license.
+
 import ..smtexpr
 import ..smtcompile
 import ..bitvector

src/spec/lemmas_basic.lean

@@ -1,3 +1,6 @@
+-- Copyright (c) Microsoft Corporation. All rights reserved.
+-- Licensed under the MIT license.
+
 universes u v
 -- Basic
 lemma prod_inj: ∀ {α:Type u} {β:Type v} (p q:α × β),

src/spec/openprog.lean

@@ -1,3 +1,6 @@
+-- Copyright (c) Microsoft Corporation. All rights reserved.
+-- Licensed under the MIT license.
+
 import ..smtexpr
 import ..smtcompile
 import ..bitvector

src/spec/refinement.lean

@@ -1,3 +1,6 @@
+-- Copyright (c) Microsoft Corporation. All rights reserved.
+-- Licensed under the MIT license.
+
 import ..smtexpr
 import ..smtcompile
 import ..bitvector

src/spec/spec.lean

@@ -1,3 +1,6 @@
+-- Copyright (c) Microsoft Corporation. All rights reserved.
+-- Licensed under the MIT license.
+
 import ..smtexpr
 import ..bitvector
 import ..irsem

src/vcgen.lean

@@ -1,3 +1,6 @@
+-- Copyright (c) Microsoft Corporation. All rights reserved.
+-- Licensed under the MIT license.
+
 import .lang
 import .irsem
 import .irsem_exec

src/verifyopt.lean

@@ -1,3 +1,6 @@
+-- Copyright (c) Microsoft Corporation. All rights reserved.
+-- Licensed under the MIT license.
+
 import .ops
 import .lang
 import .irsem