add license crap

LICENSE

+
+All files in this development are
+distributed under the terms of the 3-clause BSD license
+(https://opensource.org/licenses/BSD-3-Clause), included below.
+
+Copyright: Iris developers and Simuliris developers 
+
+------------------------------------------------------------------------------
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+    * Redistributions of source code must retain the above copyright
+      notice, this list of conditions and the following disclaimer.
+    * Redistributions in binary form must reproduce the above copyright
+      notice, this list of conditions and the following disclaimer in the
+      documentation and/or other materials provided with the distribution.
+    * Neither the name of the copyright holder nor the names of its contributors
+      may be used to endorse or promote products derived from this software
+      without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND
+ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
+WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
+DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE FOR
+ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
+(INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
+LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON
+ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

theories/base_logic/gen_heap_bij.v

@@ -6,26 +6,6 @@ From iris.algebra.lib Require Import gset_bij.
 
 
 (** * General ghost state construction that provides assertions that particular parts of the source and target heaps are in a bijection *)
-
-
-Section gset_bij.
-  Context `{gset_bijG Σ A B}.
-  Implicit Types (L : gset (A * B)) (a : A) (b : B).
-
-  (* TODO: maybe upstream into Iris?*)
-  Lemma gset_bij_own_elem_auth_agree {γ q L} a b :
-    gset_bij_own_auth γ q L -∗ gset_bij_own_elem γ a b -∗ ⌜(a, b) ∈ L⌝.
-  Proof.
-    iIntros "Hauth Helem". rewrite gset_bij_own_auth_eq gset_bij_own_elem_eq.
-    (* TODO: is there a more elegant way to do this? *)
-    iPoseProof (own_op with "[$Hauth $Helem]") as "Ha".
-    iPoseProof (own_valid_r with "Ha") as "[Ha %Hval]".
-    iPoseProof (own_op with "Ha") as "[Hauth Helem]".
-    iFrame. iPureIntro. revert Hval. rewrite bij_both_dfrac_valid.
-    intros (_ & _ & ?); done.
-  Qed.
-End gset_bij.
-
 Class gen_heap_bijGpreS `{gen_sim_heapGS L_t L_s V_t V_s Σ} := GenHeapBijGPreS {
   gen_heap_bij_pre_bijG :> gset_bijG Σ L_t L_s;
 }.
@@ -95,7 +75,7 @@ Section laws.
         gen_heap_bij_inv val_rel).
   Proof.
     iIntros "Hinv Hrel". iDestruct "Hinv" as (L) "[Hauth Hheap]".
-    iPoseProof (gset_bij_own_elem_auth_agree with "Hauth Hrel") as "%".
+    iPoseProof (gset_bij_elem_of with "Hauth Hrel") as "%".
     iPoseProof (big_sepS_delete with "Hheap") as "[He Hheap]"; first done.
     iDestruct "He" as (v_t v_s) "(H_t & H_s & Hvrel)".
     iExists v_t, v_s. iFrame.

theories/base_logic/gen_sim_heap.v

+(** This file has been adapted from the Iris development, available at 
+  https://gitlab.mpi-sws.org/iris/iris
+*)
+
 From stdpp Require Export namespaces.
 From iris.algebra Require Import gmap_view reservation_map agree frac.
 From iris.algebra Require Export dfrac.

theories/logic/fixpoints.v

+(** This file has been adapted from the Iris development, available at 
+  https://gitlab.mpi-sws.org/iris/iris
+*)
+
 From iris.bi Require Export bi.
 From iris.proofmode Require Import tactics.
 From iris.prelude Require Import options.

theories/stacked_borrows/bor_semantics.v

+(** This file has been adapted from the Stacked Borrows development, available at 
+  https://gitlab.mpi-sws.org/FP/stacked-borrows
+*)
+
 From Equations Require Import Equations.
 From iris.prelude Require Import prelude options.
 From stdpp Require Export gmap.

theories/stacked_borrows/defs.v

+(** This file has been adapted from the Stacked Borrows development, available at 
+  https://gitlab.mpi-sws.org/FP/stacked-borrows
+*)
+
 From iris.prelude Require Export prelude.
 From simuliris.stacked_borrows Require Export tactics notation lang bor_semantics.
 From iris.prelude Require Import options.

theories/stacked_borrows/examples/opt1.v

+(** This file has been adapted from the Stacked Borrows development, available at 
+  https://gitlab.mpi-sws.org/FP/stacked-borrows
+*)
+
 From simuliris.simulation Require Import lifting.
 From simuliris.stacked_borrows Require Import primitive_laws proofmode adequacy examples.lib.
 From iris.prelude Require Import options.

theories/stacked_borrows/examples/opt1_down.v

+(** This file has been adapted from the Stacked Borrows development, available at 
+  https://gitlab.mpi-sws.org/FP/stacked-borrows
+*)
+
 From simuliris.simulation Require Import lifting.
 From simuliris.stacked_borrows Require Import primitive_laws proofmode examples.lib adequacy.
 From iris.prelude Require Import options.

theories/stacked_borrows/examples/opt2.v

+(** This file has been adapted from the Stacked Borrows development, available at 
+  https://gitlab.mpi-sws.org/FP/stacked-borrows
+*)
+
 From simuliris.simulation Require Import lifting.
 From simuliris.stacked_borrows Require Import proofmode lang adequacy examples.lib.
 From iris.prelude Require Import options.

theories/stacked_borrows/examples/opt2_down.v

+(** This file has been adapted from the Stacked Borrows development, available at 
+  https://gitlab.mpi-sws.org/FP/stacked-borrows
+*)
+
 From simuliris.simulation Require Import lifting.
 From simuliris.stacked_borrows Require Import proofmode lang examples.lib adequacy.
 From iris.prelude Require Import options.

theories/stacked_borrows/examples/opt3.v

+(** This file has been adapted from the Stacked Borrows development, available at 
+  https://gitlab.mpi-sws.org/FP/stacked-borrows
+*)
+
 From simuliris.simulation Require Import lifting.
 From simuliris.stacked_borrows Require Import proofmode lang adequacy examples.lib.
 From iris.prelude Require Import options.

theories/stacked_borrows/examples/opt3_down.v

+(** This file has been adapted from the Stacked Borrows development, available at 
+  https://gitlab.mpi-sws.org/FP/stacked-borrows
+*)
+
 From simuliris.simulation Require Import lifting.
 From simuliris.stacked_borrows Require Import proofmode lang adequacy examples.lib.
 From iris.prelude Require Import options.

theories/stacked_borrows/expr_semantics.v

+(** This file has been adapted from the Stacked Borrows development, available at 
+  https://gitlab.mpi-sws.org/FP/stacked-borrows
+*)
+
 From Equations Require Import Equations.
 From iris.prelude Require Import prelude options.
 From stdpp Require Export gmap.

theories/stacked_borrows/helpers.v

+(** This file has been adapted from the Stacked Borrows development, available at 
+  https://gitlab.mpi-sws.org/FP/stacked-borrows
+*)
+
 From Coq Require Import ssreflect.
 From stdpp Require Export list gmap.
 From iris.prelude Require Import options.

theories/stacked_borrows/lang.v

+(** This file has been adapted from the Stacked Borrows development, available at 
+  https://gitlab.mpi-sws.org/FP/stacked-borrows
+*)
+
 From simuliris.simulation Require Export language.
 From iris.algebra Require Import ofe.
 From iris.prelude Require Import options.

theories/stacked_borrows/lang_base.v

+(** This file has been adapted from the Stacked Borrows development, available at 
+  https://gitlab.mpi-sws.org/FP/stacked-borrows
+*)
+
 From stdpp Require Export countable binders gmap.
 From iris.prelude Require Import prelude options.
 From iris.prelude Require Import options.

theories/stacked_borrows/locations.v

+(** This file has been adapted from the Stacked Borrows development, available at 
+  https://gitlab.mpi-sws.org/FP/stacked-borrows
+*)
+
 From iris.prelude Require Import prelude.
 From iris.prelude Require Import options.
 From stdpp Require Import countable numbers gmap.

theories/stacked_borrows/notation.v

+(** This file has been adapted from the Stacked Borrows development, available at 
+  https://gitlab.mpi-sws.org/FP/stacked-borrows
+*)
+
 From iris.prelude Require Import prelude options.
 From simuliris.stacked_borrows Require Export lang_base.
 From iris.prelude Require Import options.

theories/stacked_borrows/steps_access.v

+(** This file has been adapted from the Stacked Borrows development, available at 
+  https://gitlab.mpi-sws.org/FP/stacked-borrows
+*)
+
 From simuliris.stacked_borrows Require Export defs steps_foreach steps_list.
 From iris.prelude Require Import options.
 

theories/stacked_borrows/steps_foreach.v

+(** This file has been adapted from the Stacked Borrows development, available at 
+  https://gitlab.mpi-sws.org/FP/stacked-borrows
+*)
+
 From simuliris.stacked_borrows Require Export defs.
 From iris.prelude Require Import options.