diff --git a/system-semantics/Common/CBase.v b/system-semantics/Common/CBase.v index 8556db3..69860bc 100644 --- a/system-semantics/Common/CBase.v +++ b/system-semantics/Common/CBase.v @@ -1,3 +1,41 @@ +(* *) +(* BSD 2-clause License *) +(* *) +(* This applies to all files in this archive except where *) +(* specified otherwise. *) +(* *) +(* Copyright (c) 2022 *) +(* Thibaut Pérami *) +(* Jean Pichon-Pharabod *) +(* Brian Campbell *) +(* Alasdair Armstrong *) +(* Ben Simner *) +(* Peter Sewell *) +(* *) +(* All rights reserved. *) +(* *) +(* 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. *) +(* *) +(* 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. *) +(* *) From stdpp Require Export base. From stdpp Require Export tactics. diff --git a/system-semantics/Common/CBitvector.v b/system-semantics/Common/CBitvector.v index 0a9b838..82cc774 100644 --- a/system-semantics/Common/CBitvector.v +++ b/system-semantics/Common/CBitvector.v @@ -1,3 +1,42 @@ +(* *) +(* BSD 2-clause License *) +(* *) +(* This applies to all files in this archive except where *) +(* specified otherwise. *) +(* *) +(* Copyright (c) 2022 *) +(* Thibaut Pérami *) +(* Jean Pichon-Pharabod *) +(* Brian Campbell *) +(* Alasdair Armstrong *) +(* Ben Simner *) +(* Peter Sewell *) +(* *) +(* All rights reserved. *) +(* *) +(* 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. *) +(* *) +(* 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. *) +(* *) + (** Unfortunately this development needs to support two kinds of bitvector. The module will attempt to provide smooth interoperability between the two *) diff --git a/system-semantics/Common/CBool.v b/system-semantics/Common/CBool.v index de1a3e5..8969050 100644 --- a/system-semantics/Common/CBool.v +++ b/system-semantics/Common/CBool.v @@ -1,3 +1,42 @@ +(* *) +(* BSD 2-clause License *) +(* *) +(* This applies to all files in this archive except where *) +(* specified otherwise. *) +(* *) +(* Copyright (c) 2022 *) +(* Thibaut Pérami *) +(* Jean Pichon-Pharabod *) +(* Brian Campbell *) +(* Alasdair Armstrong *) +(* Ben Simner *) +(* Peter Sewell *) +(* *) +(* All rights reserved. *) +(* *) +(* 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. *) +(* *) +(* 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. *) +(* *) + (** This module cover all thing related to uses of boolean, mainly as decidable proposition. diff --git a/system-semantics/Common/CInduction.v b/system-semantics/Common/CInduction.v index f96688d..3367933 100644 --- a/system-semantics/Common/CInduction.v +++ b/system-semantics/Common/CInduction.v @@ -1,3 +1,42 @@ +(* *) +(* BSD 2-clause License *) +(* *) +(* This applies to all files in this archive except where *) +(* specified otherwise. *) +(* *) +(* Copyright (c) 2022 *) +(* Thibaut Pérami *) +(* Jean Pichon-Pharabod *) +(* Brian Campbell *) +(* Alasdair Armstrong *) +(* Ben Simner *) +(* Peter Sewell *) +(* *) +(* All rights reserved. *) +(* *) +(* 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. *) +(* *) +(* 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. *) +(* *) + Require Import Program.Tactics. Require Import Arith. Require Import CBase. diff --git a/system-semantics/Common/CList.v b/system-semantics/Common/CList.v index afbd033..48e2cb8 100644 --- a/system-semantics/Common/CList.v +++ b/system-semantics/Common/CList.v @@ -1,3 +1,42 @@ +(* *) +(* BSD 2-clause License *) +(* *) +(* This applies to all files in this archive except where *) +(* specified otherwise. *) +(* *) +(* Copyright (c) 2022 *) +(* Thibaut Pérami *) +(* Jean Pichon-Pharabod *) +(* Brian Campbell *) +(* Alasdair Armstrong *) +(* Ben Simner *) +(* Peter Sewell *) +(* *) +(* All rights reserved. *) +(* *) +(* 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. *) +(* *) +(* 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. *) +(* *) + Require Import CBase CBool CMaps. From stdpp Require Import base. From stdpp Require Export list. diff --git a/system-semantics/Common/CMaps.v b/system-semantics/Common/CMaps.v index 32f8518..316d37d 100644 --- a/system-semantics/Common/CMaps.v +++ b/system-semantics/Common/CMaps.v @@ -1,3 +1,42 @@ +(* *) +(* BSD 2-clause License *) +(* *) +(* This applies to all files in this archive except where *) +(* specified otherwise. *) +(* *) +(* Copyright (c) 2022 *) +(* Thibaut Pérami *) +(* Jean Pichon-Pharabod *) +(* Brian Campbell *) +(* Alasdair Armstrong *) +(* Ben Simner *) +(* Peter Sewell *) +(* *) +(* All rights reserved. *) +(* *) +(* 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. *) +(* *) +(* 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. *) +(* *) + From stdpp Require Export gmap. From stdpp Require Export fin_maps. diff --git a/system-semantics/Common/CSets.v b/system-semantics/Common/CSets.v index eb2c0b8..2064d38 100644 --- a/system-semantics/Common/CSets.v +++ b/system-semantics/Common/CSets.v @@ -1,3 +1,42 @@ +(* *) +(* BSD 2-clause License *) +(* *) +(* This applies to all files in this archive except where *) +(* specified otherwise. *) +(* *) +(* Copyright (c) 2022 *) +(* Thibaut Pérami *) +(* Jean Pichon-Pharabod *) +(* Brian Campbell *) +(* Alasdair Armstrong *) +(* Ben Simner *) +(* Peter Sewell *) +(* *) +(* All rights reserved. *) +(* *) +(* 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. *) +(* *) +(* 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. *) +(* *) + From stdpp Require Export sets. From stdpp Require Export gmap. (* <- contains gset *) From stdpp Require Export finite. diff --git a/system-semantics/Common/Common.v b/system-semantics/Common/Common.v index ec9f8d0..997cfc9 100644 --- a/system-semantics/Common/Common.v +++ b/system-semantics/Common/Common.v @@ -1,3 +1,42 @@ +(* *) +(* BSD 2-clause License *) +(* *) +(* This applies to all files in this archive except where *) +(* specified otherwise. *) +(* *) +(* Copyright (c) 2022 *) +(* Thibaut Pérami *) +(* Jean Pichon-Pharabod *) +(* Brian Campbell *) +(* Alasdair Armstrong *) +(* Ben Simner *) +(* Peter Sewell *) +(* *) +(* All rights reserved. *) +(* *) +(* 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. *) +(* *) +(* 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. *) +(* *) + (** This file is the top level of the SSCCommon library. Users should just Require Import SSCCommon.Common. *) diff --git a/system-semantics/Common/Exec.v b/system-semantics/Common/Exec.v index 6a36d63..7d50c99 100644 --- a/system-semantics/Common/Exec.v +++ b/system-semantics/Common/Exec.v @@ -1,3 +1,42 @@ +(* *) +(* BSD 2-clause License *) +(* *) +(* This applies to all files in this archive except where *) +(* specified otherwise. *) +(* *) +(* Copyright (c) 2022 *) +(* Thibaut Pérami *) +(* Jean Pichon-Pharabod *) +(* Brian Campbell *) +(* Alasdair Armstrong *) +(* Ben Simner *) +(* Peter Sewell *) +(* *) +(* All rights reserved. *) +(* *) +(* 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. *) +(* *) +(* 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. *) +(* *) + (* This file defines an execution monad for the model. The execution model is Either a named error or a lists of possible outputs. diff --git a/system-semantics/Common/GRel.v b/system-semantics/Common/GRel.v index d7fb5d2..197fdbb 100644 --- a/system-semantics/Common/GRel.v +++ b/system-semantics/Common/GRel.v @@ -1,3 +1,42 @@ +(* *) +(* BSD 2-clause License *) +(* *) +(* This applies to all files in this archive except where *) +(* specified otherwise. *) +(* *) +(* Copyright (c) 2022 *) +(* Thibaut Pérami *) +(* Jean Pichon-Pharabod *) +(* Brian Campbell *) +(* Alasdair Armstrong *) +(* Ben Simner *) +(* Peter Sewell *) +(* *) +(* All rights reserved. *) +(* *) +(* 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. *) +(* *) +(* 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. *) +(* *) + (** This file define a relation using a gset from stdpp that is entirely computable and whose standard relational operators are also computable. The type is [grel A] diff --git a/system-semantics/ISASem/ArmInst.v b/system-semantics/ISASem/ArmInst.v index efd0c3d..33007a5 100644 --- a/system-semantics/ISASem/ArmInst.v +++ b/system-semantics/ISASem/ArmInst.v @@ -1,3 +1,42 @@ +(* *) +(* BSD 2-clause License *) +(* *) +(* This applies to all files in this archive except where *) +(* specified otherwise. *) +(* *) +(* Copyright (c) 2022 *) +(* Thibaut Pérami *) +(* Jean Pichon-Pharabod *) +(* Brian Campbell *) +(* Alasdair Armstrong *) +(* Ben Simner *) +(* Peter Sewell *) +(* *) +(* All rights reserved. *) +(* *) +(* 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. *) +(* *) +(* 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. *) +(* *) + Require Import Strings.String. Require Import stdpp.unstable.bitvector. Require Import stdpp.strings. diff --git a/system-semantics/ISASem/Interface.v b/system-semantics/ISASem/Interface.v index 53d4e4d..0f66cbc 100644 --- a/system-semantics/ISASem/Interface.v +++ b/system-semantics/ISASem/Interface.v @@ -1,3 +1,41 @@ +(* *) +(* BSD 2-clause License *) +(* *) +(* This applies to all files in this archive except where *) +(* specified otherwise. *) +(* *) +(* Copyright (c) 2022 *) +(* Thibaut Pérami *) +(* Jean Pichon-Pharabod *) +(* Brian Campbell *) +(* Alasdair Armstrong *) +(* Ben Simner *) +(* Peter Sewell *) +(* *) +(* All rights reserved. *) +(* *) +(* 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. *) +(* *) +(* 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. *) +(* *) Require Import Strings.String. Require Import stdpp.unstable.bitvector. diff --git a/theories/CandidateExecutions.v b/theories/CandidateExecutions.v index 4da7115..08283cc 100644 --- a/theories/CandidateExecutions.v +++ b/theories/CandidateExecutions.v @@ -1,3 +1,39 @@ +(* *) +(* BSD 2-Clause License *) +(* *) +(* This applies to all files in this archive except folder *) +(* "system-semantics". *) +(* *) +(* Copyright (c) 2023, *) +(* Zongyuan Liu *) +(* Angus Hammond *) +(* Jean Pichon-Pharabod *) +(* Thibaut Pérami *) +(* *) +(* All rights reserved. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions are met: *) +(* *) +(* 1. Redistributions of source code must retain the above copyright notice, this *) +(* list of conditions and the following disclaimer. *) +(* *) +(* 2. 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. *) +(* *) +(* 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. *) +(* *) + (* Simplified version of [CandidateExecutions.v] of [system-semantics-coq]. *) (** This file provide a common type for representing candidate executions diff --git a/theories/algebra/base.v b/theories/algebra/base.v index 9d5c650..29df54e 100644 --- a/theories/algebra/base.v +++ b/theories/algebra/base.v @@ -1,3 +1,39 @@ +(* *) +(* BSD 2-Clause License *) +(* *) +(* This applies to all files in this archive except folder *) +(* "system-semantics". *) +(* *) +(* Copyright (c) 2023, *) +(* Zongyuan Liu *) +(* Angus Hammond *) +(* Jean Pichon-Pharabod *) +(* Thibaut Pérami *) +(* *) +(* All rights reserved. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions are met: *) +(* *) +(* 1. Redistributions of source code must retain the above copyright notice, this *) +(* list of conditions and the following disclaimer. *) +(* *) +(* 2. 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. *) +(* *) +(* 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. *) +(* *) + (** This file contains construction of basic RAs *) (* From stdpp Require Export namespaces. *) diff --git a/theories/algebra/ghost_map_ag.v b/theories/algebra/ghost_map_ag.v index b090392..0d9a8fb 100644 --- a/theories/algebra/ghost_map_ag.v +++ b/theories/algebra/ghost_map_ag.v @@ -1,3 +1,39 @@ +(* *) +(* BSD 2-Clause License *) +(* *) +(* This applies to all files in this archive except folder *) +(* "system-semantics". *) +(* *) +(* Copyright (c) 2023, *) +(* Zongyuan Liu *) +(* Angus Hammond *) +(* Jean Pichon-Pharabod *) +(* Thibaut Pérami *) +(* *) +(* All rights reserved. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions are met: *) +(* *) +(* 1. Redistributions of source code must retain the above copyright notice, this *) +(* list of conditions and the following disclaimer. *) +(* *) +(* 2. 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. *) +(* *) +(* 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. *) +(* *) + (** This file contains the RA of construction gmap K (agree V)*) From iris.base_logic.lib Require Export own. From iris.proofmode Require Import tactics. diff --git a/theories/algebra/lib/gmap_view_ag.v b/theories/algebra/lib/gmap_view_ag.v index d0dff64..035f8eb 100644 --- a/theories/algebra/lib/gmap_view_ag.v +++ b/theories/algebra/lib/gmap_view_ag.v @@ -1,3 +1,39 @@ +(* *) +(* BSD 2-Clause License *) +(* *) +(* This applies to all files in this archive except folder *) +(* "system-semantics". *) +(* *) +(* Copyright (c) 2023, *) +(* Zongyuan Liu *) +(* Angus Hammond *) +(* Jean Pichon-Pharabod *) +(* Thibaut Pérami *) +(* *) +(* All rights reserved. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions are met: *) +(* *) +(* 1. Redistributions of source code must retain the above copyright notice, this *) +(* list of conditions and the following disclaimer. *) +(* *) +(* 2. 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. *) +(* *) +(* 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. *) +(* *) + (** This file contains a variant of [gmap_view]: gmap K (agree V) *) (** Most of lemmas are their proofs are copied from [iris.algebra/lib/gmap_view] and tweaked *) From iris.algebra Require Export view gmap. diff --git a/theories/algebra/mono_pg.v b/theories/algebra/mono_pg.v index a7eba2b..eb7a01b 100644 --- a/theories/algebra/mono_pg.v +++ b/theories/algebra/mono_pg.v @@ -1,3 +1,39 @@ +(* *) +(* BSD 2-Clause License *) +(* *) +(* This applies to all files in this archive except folder *) +(* "system-semantics". *) +(* *) +(* Copyright (c) 2023, *) +(* Zongyuan Liu *) +(* Angus Hammond *) +(* Jean Pichon-Pharabod *) +(* Thibaut Pérami *) +(* *) +(* All rights reserved. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions are met: *) +(* *) +(* 1. Redistributions of source code must retain the above copyright notice, this *) +(* list of conditions and the following disclaimer. *) +(* *) +(* 2. 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. *) +(* *) +(* 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. *) +(* *) + From iris.algebra Require Export auth. From iris.algebra Require Import numbers updates. From iris.prelude Require Import options. diff --git a/theories/cmra.v b/theories/cmra.v index 8a023ef..4194f81 100644 --- a/theories/cmra.v +++ b/theories/cmra.v @@ -1,3 +1,39 @@ +(* *) +(* BSD 2-Clause License *) +(* *) +(* This applies to all files in this archive except folder *) +(* "system-semantics". *) +(* *) +(* Copyright (c) 2023, *) +(* Zongyuan Liu *) +(* Angus Hammond *) +(* Jean Pichon-Pharabod *) +(* Thibaut Pérami *) +(* *) +(* All rights reserved. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions are met: *) +(* *) +(* 1. Redistributions of source code must retain the above copyright notice, this *) +(* list of conditions and the following disclaimer. *) +(* *) +(* 2. 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. *) +(* *) +(* 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. *) +(* *) + (* This file contains the [CMRA] typeclass that is used by both the logic construction and the RAs *) From iris.base_logic.lib Require Export iprop. diff --git a/theories/examples/co/corr.v b/theories/examples/co/corr.v index 6810b29..6da3a5d 100644 --- a/theories/examples/co/corr.v +++ b/theories/examples/co/corr.v @@ -1,3 +1,39 @@ +(* *) +(* BSD 2-Clause License *) +(* *) +(* This applies to all files in this archive except folder *) +(* "system-semantics". *) +(* *) +(* Copyright (c) 2023, *) +(* Zongyuan Liu *) +(* Angus Hammond *) +(* Jean Pichon-Pharabod *) +(* Thibaut Pérami *) +(* *) +(* All rights reserved. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions are met: *) +(* *) +(* 1. Redistributions of source code must retain the above copyright notice, this *) +(* list of conditions and the following disclaimer. *) +(* *) +(* 2. 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. *) +(* *) +(* 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. *) +(* *) + From stdpp.unstable Require Import bitvector bitvector_tactics. From iris.proofmode Require Import tactics. diff --git a/theories/examples/co/coww.v b/theories/examples/co/coww.v index 401b503..74bbc48 100644 --- a/theories/examples/co/coww.v +++ b/theories/examples/co/coww.v @@ -1,3 +1,39 @@ +(* *) +(* BSD 2-Clause License *) +(* *) +(* This applies to all files in this archive except folder *) +(* "system-semantics". *) +(* *) +(* Copyright (c) 2023, *) +(* Zongyuan Liu *) +(* Angus Hammond *) +(* Jean Pichon-Pharabod *) +(* Thibaut Pérami *) +(* *) +(* All rights reserved. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions are met: *) +(* *) +(* 1. Redistributions of source code must retain the above copyright notice, this *) +(* list of conditions and the following disclaimer. *) +(* *) +(* 2. 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. *) +(* *) +(* 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. *) +(* *) + From stdpp.unstable Require Import bitvector bitvector_tactics. From iris.proofmode Require Import tactics. diff --git a/theories/examples/isa2/isa2.v b/theories/examples/isa2/isa2.v index 8e96940..a4921fd 100644 --- a/theories/examples/isa2/isa2.v +++ b/theories/examples/isa2/isa2.v @@ -1,3 +1,39 @@ +(* *) +(* BSD 2-Clause License *) +(* *) +(* This applies to all files in this archive except folder *) +(* "system-semantics". *) +(* *) +(* Copyright (c) 2023, *) +(* Zongyuan Liu *) +(* Angus Hammond *) +(* Jean Pichon-Pharabod *) +(* Thibaut Pérami *) +(* *) +(* All rights reserved. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions are met: *) +(* *) +(* 1. Redistributions of source code must retain the above copyright notice, this *) +(* list of conditions and the following disclaimer. *) +(* *) +(* 2. 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. *) +(* *) +(* 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. *) +(* *) + From stdpp.unstable Require Import bitvector bitvector_tactics. From iris.proofmode Require Import tactics. diff --git a/theories/examples/lb/adequacy.v b/theories/examples/lb/adequacy.v index 10e2809..20b76cc 100644 --- a/theories/examples/lb/adequacy.v +++ b/theories/examples/lb/adequacy.v @@ -1,3 +1,39 @@ +(* *) +(* BSD 2-Clause License *) +(* *) +(* This applies to all files in this archive except folder *) +(* "system-semantics". *) +(* *) +(* Copyright (c) 2023, *) +(* Zongyuan Liu *) +(* Angus Hammond *) +(* Jean Pichon-Pharabod *) +(* Thibaut Pérami *) +(* *) +(* All rights reserved. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions are met: *) +(* *) +(* 1. Redistributions of source code must retain the above copyright notice, this *) +(* list of conditions and the following disclaimer. *) +(* *) +(* 2. 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. *) +(* *) +(* 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. *) +(* *) + (* This file contains an application of adequacy theorem on the [data_data1] example *) From iris.proofmode Require Import tactics. diff --git a/theories/examples/lb/ctrls.v b/theories/examples/lb/ctrls.v index cbc7dce..9cfb965 100644 --- a/theories/examples/lb/ctrls.v +++ b/theories/examples/lb/ctrls.v @@ -1,3 +1,39 @@ +(* *) +(* BSD 2-Clause License *) +(* *) +(* This applies to all files in this archive except folder *) +(* "system-semantics". *) +(* *) +(* Copyright (c) 2023, *) +(* Zongyuan Liu *) +(* Angus Hammond *) +(* Jean Pichon-Pharabod *) +(* Thibaut Pérami *) +(* *) +(* All rights reserved. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions are met: *) +(* *) +(* 1. Redistributions of source code must retain the above copyright notice, this *) +(* list of conditions and the following disclaimer. *) +(* *) +(* 2. 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. *) +(* *) +(* 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. *) +(* *) + From stdpp.unstable Require Import bitvector bitvector_tactics. From iris.proofmode Require Import tactics. diff --git a/theories/examples/lb/data_data1.v b/theories/examples/lb/data_data1.v index 6b660c2..b473938 100644 --- a/theories/examples/lb/data_data1.v +++ b/theories/examples/lb/data_data1.v @@ -1,3 +1,39 @@ +(* *) +(* BSD 2-Clause License *) +(* *) +(* This applies to all files in this archive except folder *) +(* "system-semantics". *) +(* *) +(* Copyright (c) 2023, *) +(* Zongyuan Liu *) +(* Angus Hammond *) +(* Jean Pichon-Pharabod *) +(* Thibaut Pérami *) +(* *) +(* All rights reserved. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions are met: *) +(* *) +(* 1. Redistributions of source code must retain the above copyright notice, this *) +(* list of conditions and the following disclaimer. *) +(* *) +(* 2. 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. *) +(* *) +(* 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. *) +(* *) + From stdpp.unstable Require Export bitvector. From stdpp.unstable Require Import bitvector_tactics. diff --git a/theories/examples/lb/data_data2.v b/theories/examples/lb/data_data2.v index ac28494..20d068f 100644 --- a/theories/examples/lb/data_data2.v +++ b/theories/examples/lb/data_data2.v @@ -1,3 +1,39 @@ +(* *) +(* BSD 2-Clause License *) +(* *) +(* This applies to all files in this archive except folder *) +(* "system-semantics". *) +(* *) +(* Copyright (c) 2023, *) +(* Zongyuan Liu *) +(* Angus Hammond *) +(* Jean Pichon-Pharabod *) +(* Thibaut Pérami *) +(* *) +(* All rights reserved. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions are met: *) +(* *) +(* 1. Redistributions of source code must retain the above copyright notice, this *) +(* list of conditions and the following disclaimer. *) +(* *) +(* 2. 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. *) +(* *) +(* 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. *) +(* *) + From stdpp.unstable Require Import bitvector bitvector_tactics. From iris.proofmode Require Import tactics. diff --git a/theories/examples/lb/data_dmbsy.v b/theories/examples/lb/data_dmbsy.v index a3427bf..eb3fe26 100644 --- a/theories/examples/lb/data_dmbsy.v +++ b/theories/examples/lb/data_dmbsy.v @@ -1,3 +1,39 @@ +(* *) +(* BSD 2-Clause License *) +(* *) +(* This applies to all files in this archive except folder *) +(* "system-semantics". *) +(* *) +(* Copyright (c) 2023, *) +(* Zongyuan Liu *) +(* Angus Hammond *) +(* Jean Pichon-Pharabod *) +(* Thibaut Pérami *) +(* *) +(* All rights reserved. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions are met: *) +(* *) +(* 1. Redistributions of source code must retain the above copyright notice, this *) +(* list of conditions and the following disclaimer. *) +(* *) +(* 2. 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. *) +(* *) +(* 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. *) +(* *) + From stdpp.unstable Require Import bitvector bitvector_tactics. From iris.proofmode Require Import tactics. diff --git a/theories/examples/mp/rel_acq.v b/theories/examples/mp/rel_acq.v index eae86d7..b1d6efe 100644 --- a/theories/examples/mp/rel_acq.v +++ b/theories/examples/mp/rel_acq.v @@ -1,3 +1,39 @@ +(* *) +(* BSD 2-Clause License *) +(* *) +(* This applies to all files in this archive except folder *) +(* "system-semantics". *) +(* *) +(* Copyright (c) 2023, *) +(* Zongyuan Liu *) +(* Angus Hammond *) +(* Jean Pichon-Pharabod *) +(* Thibaut Pérami *) +(* *) +(* All rights reserved. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions are met: *) +(* *) +(* 1. Redistributions of source code must retain the above copyright notice, this *) +(* list of conditions and the following disclaimer. *) +(* *) +(* 2. 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. *) +(* *) +(* 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. *) +(* *) + From stdpp.unstable Require Import bitvector bitvector_tactics. From iris.proofmode Require Import tactics. diff --git a/theories/examples/mp/rel_addr.v b/theories/examples/mp/rel_addr.v index c9fe128..d412eec 100644 --- a/theories/examples/mp/rel_addr.v +++ b/theories/examples/mp/rel_addr.v @@ -1,3 +1,39 @@ +(* *) +(* BSD 2-Clause License *) +(* *) +(* This applies to all files in this archive except folder *) +(* "system-semantics". *) +(* *) +(* Copyright (c) 2023, *) +(* Zongyuan Liu *) +(* Angus Hammond *) +(* Jean Pichon-Pharabod *) +(* Thibaut Pérami *) +(* *) +(* All rights reserved. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions are met: *) +(* *) +(* 1. Redistributions of source code must retain the above copyright notice, this *) +(* list of conditions and the following disclaimer. *) +(* *) +(* 2. 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. *) +(* *) +(* 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. *) +(* *) + From stdpp.unstable Require Import bitvector bitvector_tactics. From iris.proofmode Require Import tactics. diff --git a/theories/examples/mp/rel_ctrl.v b/theories/examples/mp/rel_ctrl.v index ad4e8a1..af6900a 100644 --- a/theories/examples/mp/rel_ctrl.v +++ b/theories/examples/mp/rel_ctrl.v @@ -1,3 +1,38 @@ +(* *) +(* BSD 2-Clause License *) +(* *) +(* This applies to all files in this archive except folder *) +(* "system-semantics". *) +(* *) +(* Copyright (c) 2023, *) +(* Zongyuan Liu *) +(* Angus Hammond *) +(* Jean Pichon-Pharabod *) +(* Thibaut Pérami *) +(* *) +(* All rights reserved. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions are met: *) +(* *) +(* 1. Redistributions of source code must retain the above copyright notice, this *) +(* list of conditions and the following disclaimer. *) +(* *) +(* 2. 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. *) +(* *) +(* 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. *) +(* *) From stdpp.unstable Require Import bitvector bitvector_tactics. diff --git a/theories/examples/mp/rel_dmb.v b/theories/examples/mp/rel_dmb.v index e0ed9aa..b68410e 100644 --- a/theories/examples/mp/rel_dmb.v +++ b/theories/examples/mp/rel_dmb.v @@ -1,3 +1,39 @@ +(* *) +(* BSD 2-Clause License *) +(* *) +(* This applies to all files in this archive except folder *) +(* "system-semantics". *) +(* *) +(* Copyright (c) 2023, *) +(* Zongyuan Liu *) +(* Angus Hammond *) +(* Jean Pichon-Pharabod *) +(* Thibaut Pérami *) +(* *) +(* All rights reserved. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions are met: *) +(* *) +(* 1. Redistributions of source code must retain the above copyright notice, this *) +(* list of conditions and the following disclaimer. *) +(* *) +(* 2. 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. *) +(* *) +(* 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. *) +(* *) + From stdpp.unstable Require Import bitvector bitvector_tactics. From iris.proofmode Require Import tactics. diff --git a/theories/examples/try_lock/implementation.v b/theories/examples/try_lock/implementation.v index acc3dd1..7fe0ca8 100644 --- a/theories/examples/try_lock/implementation.v +++ b/theories/examples/try_lock/implementation.v @@ -1,3 +1,39 @@ +(* *) +(* BSD 2-Clause License *) +(* *) +(* This applies to all files in this archive except folder *) +(* "system-semantics". *) +(* *) +(* Copyright (c) 2023, *) +(* Zongyuan Liu *) +(* Angus Hammond *) +(* Jean Pichon-Pharabod *) +(* Thibaut Pérami *) +(* *) +(* All rights reserved. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions are met: *) +(* *) +(* 1. Redistributions of source code must retain the above copyright notice, this *) +(* list of conditions and the following disclaimer. *) +(* *) +(* 2. 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. *) +(* *) +(* 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. *) +(* *) + From stdpp.unstable Require Export bitvector. From stdpp.unstable Require Import bitvector_tactics. diff --git a/theories/examples/try_lock/mutual_exclusion.v b/theories/examples/try_lock/mutual_exclusion.v index c94f371..920dd55 100644 --- a/theories/examples/try_lock/mutual_exclusion.v +++ b/theories/examples/try_lock/mutual_exclusion.v @@ -1,3 +1,39 @@ +(* *) +(* BSD 2-Clause License *) +(* *) +(* This applies to all files in this archive except folder *) +(* "system-semantics". *) +(* *) +(* Copyright (c) 2023, *) +(* Zongyuan Liu *) +(* Angus Hammond *) +(* Jean Pichon-Pharabod *) +(* Thibaut Pérami *) +(* *) +(* All rights reserved. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions are met: *) +(* *) +(* 1. Redistributions of source code must retain the above copyright notice, this *) +(* list of conditions and the following disclaimer. *) +(* *) +(* 2. 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. *) +(* *) +(* 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. *) +(* *) + From stdpp.unstable Require Import bitvector bitvector_tactics. From iris.proofmode Require Import tactics. diff --git a/theories/iris_extra.v b/theories/iris_extra.v index f0f3d85..40eddd3 100644 --- a/theories/iris_extra.v +++ b/theories/iris_extra.v @@ -1,3 +1,39 @@ +(* *) +(* BSD 2-Clause License *) +(* *) +(* This applies to all files in this archive except folder *) +(* "system-semantics". *) +(* *) +(* Copyright (c) 2023, *) +(* Zongyuan Liu *) +(* Angus Hammond *) +(* Jean Pichon-Pharabod *) +(* Thibaut Pérami *) +(* *) +(* All rights reserved. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions are met: *) +(* *) +(* 1. Redistributions of source code must retain the above copyright notice, this *) +(* list of conditions and the following disclaimer. *) +(* *) +(* 2. 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. *) +(* *) +(* 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. *) +(* *) + From iris.bi Require Import big_op. From iris.prelude Require Import options. From iris.bi Require Import telescopes derived_laws_later. diff --git a/theories/lang/instrs.v b/theories/lang/instrs.v index 4fd0122..825ab1b 100644 --- a/theories/lang/instrs.v +++ b/theories/lang/instrs.v @@ -1,3 +1,39 @@ +(* *) +(* BSD 2-Clause License *) +(* *) +(* This applies to all files in this archive except folder *) +(* "system-semantics". *) +(* *) +(* Copyright (c) 2023, *) +(* Zongyuan Liu *) +(* Angus Hammond *) +(* Jean Pichon-Pharabod *) +(* Thibaut Pérami *) +(* *) +(* All rights reserved. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions are met: *) +(* *) +(* 1. Redistributions of source code must retain the above copyright notice, this *) +(* list of conditions and the following disclaimer. *) +(* *) +(* 2. 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. *) +(* *) +(* 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. *) +(* *) + (* This file contains the instruction semantics *) Require Import Strings.String. (* to use monad notations *) diff --git a/theories/lang/machine.v b/theories/lang/machine.v index b5b2d62..f61bef3 100644 --- a/theories/lang/machine.v +++ b/theories/lang/machine.v @@ -1,3 +1,39 @@ +(* *) +(* BSD 2-Clause License *) +(* *) +(* This applies to all files in this archive except folder *) +(* "system-semantics". *) +(* *) +(* Copyright (c) 2023, *) +(* Zongyuan Liu *) +(* Angus Hammond *) +(* Jean Pichon-Pharabod *) +(* Thibaut Pérami *) +(* *) +(* All rights reserved. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions are met: *) +(* *) +(* 1. Redistributions of source code must retain the above copyright notice, this *) +(* list of conditions and the following disclaimer. *) +(* *) +(* 2. 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. *) +(* *) +(* 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. *) +(* *) + (** This file includes our instantiation of [CandidateExecutions], and wrappers for types of [system-semantics-coq] *) Require Import stdpp.strings. diff --git a/theories/lang/mm.v b/theories/lang/mm.v index 80378c7..3021732 100644 --- a/theories/lang/mm.v +++ b/theories/lang/mm.v @@ -1,3 +1,39 @@ +(* *) +(* BSD 2-Clause License *) +(* *) +(* This applies to all files in this archive except folder *) +(* "system-semantics". *) +(* *) +(* Copyright (c) 2023, *) +(* Zongyuan Liu *) +(* Angus Hammond *) +(* Jean Pichon-Pharabod *) +(* Thibaut Pérami *) +(* *) +(* All rights reserved. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions are met: *) +(* *) +(* 1. Redistributions of source code must retain the above copyright notice, this *) +(* list of conditions and the following disclaimer. *) +(* *) +(* 2. 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. *) +(* *) +(* 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. *) +(* *) + (* This file contains the memory model *) diff --git a/theories/lang/opsem.v b/theories/lang/opsem.v index ead7ab9..814b64d 100644 --- a/theories/lang/opsem.v +++ b/theories/lang/opsem.v @@ -1,3 +1,39 @@ +(* *) +(* BSD 2-Clause License *) +(* *) +(* This applies to all files in this archive except folder *) +(* "system-semantics". *) +(* *) +(* Copyright (c) 2023, *) +(* Zongyuan Liu *) +(* Angus Hammond *) +(* Jean Pichon-Pharabod *) +(* Thibaut Pérami *) +(* *) +(* All rights reserved. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions are met: *) +(* *) +(* 1. Redistributions of source code must retain the above copyright notice, this *) +(* list of conditions and the following disclaimer. *) +(* *) +(* 2. 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. *) +(* *) +(* 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. *) +(* *) + (** This file contains the definition of the operational semantics *) From Coq Require Import ssreflect. From stdpp Require Import numbers unstable.bitvector. diff --git a/theories/low/adequacy.v b/theories/low/adequacy.v index ba14a72..08eb2e7 100644 --- a/theories/low/adequacy.v +++ b/theories/low/adequacy.v @@ -1,3 +1,39 @@ +(* *) +(* BSD 2-Clause License *) +(* *) +(* This applies to all files in this archive except folder *) +(* "system-semantics". *) +(* *) +(* Copyright (c) 2023, *) +(* Zongyuan Liu *) +(* Angus Hammond *) +(* Jean Pichon-Pharabod *) +(* Thibaut Pérami *) +(* *) +(* All rights reserved. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions are met: *) +(* *) +(* 1. Redistributions of source code must retain the above copyright notice, this *) +(* list of conditions and the following disclaimer. *) +(* *) +(* 2. 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. *) +(* *) +(* 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. *) +(* *) + From iris.proofmode Require Import tactics. From iris.base_logic.lib Require Import wsat. From self.low Require Export weakestpre. diff --git a/theories/low/instantiation.v b/theories/low/instantiation.v index 2e81547..6e99189 100644 --- a/theories/low/instantiation.v +++ b/theories/low/instantiation.v @@ -1,3 +1,39 @@ +(* *) +(* BSD 2-Clause License *) +(* *) +(* This applies to all files in this archive except folder *) +(* "system-semantics". *) +(* *) +(* Copyright (c) 2023, *) +(* Zongyuan Liu *) +(* Angus Hammond *) +(* Jean Pichon-Pharabod *) +(* Thibaut Pérami *) +(* *) +(* All rights reserved. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions are met: *) +(* *) +(* 1. Redistributions of source code must retain the above copyright notice, this *) +(* list of conditions and the following disclaimer. *) +(* *) +(* 2. 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. *) +(* *) +(* 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. *) +(* *) + (** This file contains the instantiation of the low-level logic, this is the file that all helper files import*) From iris_named_props Require Export named_props. diff --git a/theories/low/interp_mod.v b/theories/low/interp_mod.v index cfa5543..cd5ab7e 100644 --- a/theories/low/interp_mod.v +++ b/theories/low/interp_mod.v @@ -1,3 +1,39 @@ +(* *) +(* BSD 2-Clause License *) +(* *) +(* This applies to all files in this archive except folder *) +(* "system-semantics". *) +(* *) +(* Copyright (c) 2023, *) +(* Zongyuan Liu *) +(* Angus Hammond *) +(* Jean Pichon-Pharabod *) +(* Thibaut Pérami *) +(* *) +(* All rights reserved. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions are met: *) +(* *) +(* 1. Redistributions of source code must retain the above copyright notice, this *) +(* list of conditions and the following disclaimer. *) +(* *) +(* 2. 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. *) +(* *) +(* 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. *) +(* *) + (* The file contains the [interp_mod] modality, which allows one to access [annot_interp] with a basic update modality *) From iris.proofmode Require Import base tactics classes. diff --git a/theories/low/iris.v b/theories/low/iris.v index 7ef37ff..9fb3260 100644 --- a/theories/low/iris.v +++ b/theories/low/iris.v @@ -1,3 +1,39 @@ +(* *) +(* BSD 2-Clause License *) +(* *) +(* This applies to all files in this archive except folder *) +(* "system-semantics". *) +(* *) +(* Copyright (c) 2023, *) +(* Zongyuan Liu *) +(* Angus Hammond *) +(* Jean Pichon-Pharabod *) +(* Thibaut Pérami *) +(* *) +(* All rights reserved. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions are met: *) +(* *) +(* 1. Redistributions of source code must retain the above copyright notice, this *) +(* list of conditions and the following disclaimer. *) +(* *) +(* 2. 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. *) +(* *) +(* 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. *) +(* *) + (* This file contains the typeclass which is the parameter of the low-level logic, the weakest precondition and adequacy can be instantiated by any instance of the typeclass*) From iris.base_logic.lib Require Export fancy_updates. diff --git a/theories/low/lib/annotations.v b/theories/low/lib/annotations.v index 336904d..d5c979f 100644 --- a/theories/low/lib/annotations.v +++ b/theories/low/lib/annotations.v @@ -1,3 +1,39 @@ +(* *) +(* BSD 2-Clause License *) +(* *) +(* This applies to all files in this archive except folder *) +(* "system-semantics". *) +(* *) +(* Copyright (c) 2023, *) +(* Zongyuan Liu *) +(* Angus Hammond *) +(* Jean Pichon-Pharabod *) +(* Thibaut Pérami *) +(* *) +(* All rights reserved. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions are met: *) +(* *) +(* 1. Redistributions of source code must retain the above copyright notice, this *) +(* list of conditions and the following disclaimer. *) +(* *) +(* 2. 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. *) +(* *) +(* 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. *) +(* *) + (* This file contains the definition of edge annotation and node annotation, which are used by weakestpres *) From iris.algebra Require Import gmap gset. From iris.base_logic.lib Require Import fancy_updates. diff --git a/theories/low/lib/edge.v b/theories/low/lib/edge.v index 827b363..3fe23d4 100644 --- a/theories/low/lib/edge.v +++ b/theories/low/lib/edge.v @@ -1,3 +1,39 @@ +(* *) +(* BSD 2-Clause License *) +(* *) +(* This applies to all files in this archive except folder *) +(* "system-semantics". *) +(* *) +(* Copyright (c) 2023, *) +(* Zongyuan Liu *) +(* Angus Hammond *) +(* Jean Pichon-Pharabod *) +(* Thibaut Pérami *) +(* *) +(* All rights reserved. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions are met: *) +(* *) +(* 1. Redistributions of source code must retain the above copyright notice, this *) +(* list of conditions and the following disclaimer. *) +(* *) +(* 2. 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. *) +(* *) +(* 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. *) +(* *) + (* This file contains the resource construction for edges *) From SSCCommon Require Import Common. From iris.base_logic Require Import iprop. diff --git a/theories/low/lib/event.v b/theories/low/lib/event.v index 6e64be5..0323e69 100644 --- a/theories/low/lib/event.v +++ b/theories/low/lib/event.v @@ -1,3 +1,39 @@ +(* *) +(* BSD 2-Clause License *) +(* *) +(* This applies to all files in this archive except folder *) +(* "system-semantics". *) +(* *) +(* Copyright (c) 2023, *) +(* Zongyuan Liu *) +(* Angus Hammond *) +(* Jean Pichon-Pharabod *) +(* Thibaut Pérami *) +(* *) +(* All rights reserved. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions are met: *) +(* *) +(* 1. Redistributions of source code must retain the above copyright notice, this *) +(* list of conditions and the following disclaimer. *) +(* *) +(* 2. 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. *) +(* *) +(* 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. *) +(* *) + Require Import stdpp.unstable.bitvector. From SSCCommon Require Import Common. diff --git a/theories/low/lifting.v b/theories/low/lifting.v index da5c70e..17fd48a 100644 --- a/theories/low/lifting.v +++ b/theories/low/lifting.v @@ -1,3 +1,39 @@ +(* *) +(* BSD 2-Clause License *) +(* *) +(* This applies to all files in this archive except folder *) +(* "system-semantics". *) +(* *) +(* Copyright (c) 2023, *) +(* Zongyuan Liu *) +(* Angus Hammond *) +(* Jean Pichon-Pharabod *) +(* Thibaut Pérami *) +(* *) +(* All rights reserved. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions are met: *) +(* *) +(* 1. Redistributions of source code must retain the above copyright notice, this *) +(* list of conditions and the following disclaimer. *) +(* *) +(* 2. 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. *) +(* *) +(* 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. *) +(* *) + From iris.proofmode Require Import tactics. From self.low Require Export weakestpre. diff --git a/theories/low/rules/announce.v b/theories/low/rules/announce.v index 348cd69..9d422eb 100644 --- a/theories/low/rules/announce.v +++ b/theories/low/rules/announce.v @@ -1,3 +1,39 @@ +(* *) +(* BSD 2-Clause License *) +(* *) +(* This applies to all files in this archive except folder *) +(* "system-semantics". *) +(* *) +(* Copyright (c) 2023, *) +(* Zongyuan Liu *) +(* Angus Hammond *) +(* Jean Pichon-Pharabod *) +(* Thibaut Pérami *) +(* *) +(* All rights reserved. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions are met: *) +(* *) +(* 1. Redistributions of source code must retain the above copyright notice, this *) +(* list of conditions and the following disclaimer. *) +(* *) +(* 2. 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. *) +(* *) +(* 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. *) +(* *) + From self.low.rules Require Import prelude. Import uPred. diff --git a/theories/low/rules/barrier.v b/theories/low/rules/barrier.v index 25177b0..064a59f 100644 --- a/theories/low/rules/barrier.v +++ b/theories/low/rules/barrier.v @@ -1,3 +1,39 @@ +(* *) +(* BSD 2-Clause License *) +(* *) +(* This applies to all files in this archive except folder *) +(* "system-semantics". *) +(* *) +(* Copyright (c) 2023, *) +(* Zongyuan Liu *) +(* Angus Hammond *) +(* Jean Pichon-Pharabod *) +(* Thibaut Pérami *) +(* *) +(* All rights reserved. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions are met: *) +(* *) +(* 1. Redistributions of source code must retain the above copyright notice, this *) +(* list of conditions and the following disclaimer. *) +(* *) +(* 2. 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. *) +(* *) +(* 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. *) +(* *) + (* This file contains the low-level proof rules for memory barriers *) From self.low.rules Require Import prelude. diff --git a/theories/low/rules/prelude.v b/theories/low/rules/prelude.v index fb95948..b444d3d 100644 --- a/theories/low/rules/prelude.v +++ b/theories/low/rules/prelude.v @@ -1,3 +1,39 @@ +(* *) +(* BSD 2-Clause License *) +(* *) +(* This applies to all files in this archive except folder *) +(* "system-semantics". *) +(* *) +(* Copyright (c) 2023, *) +(* Zongyuan Liu *) +(* Angus Hammond *) +(* Jean Pichon-Pharabod *) +(* Thibaut Pérami *) +(* *) +(* All rights reserved. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions are met: *) +(* *) +(* 1. Redistributions of source code must retain the above copyright notice, this *) +(* list of conditions and the following disclaimer. *) +(* *) +(* 2. 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. *) +(* *) +(* 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. *) +(* *) + (* This file contains the helper tactics and lemmas that are useful for showing proof rules *) From stdpp Require Export unstable.bitvector. diff --git a/theories/low/rules/read.v b/theories/low/rules/read.v index 36efc2a..9909179 100644 --- a/theories/low/rules/read.v +++ b/theories/low/rules/read.v @@ -1,3 +1,39 @@ +(* *) +(* BSD 2-Clause License *) +(* *) +(* This applies to all files in this archive except folder *) +(* "system-semantics". *) +(* *) +(* Copyright (c) 2023, *) +(* Zongyuan Liu *) +(* Angus Hammond *) +(* Jean Pichon-Pharabod *) +(* Thibaut Pérami *) +(* *) +(* All rights reserved. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions are met: *) +(* *) +(* 1. Redistributions of source code must retain the above copyright notice, this *) +(* list of conditions and the following disclaimer. *) +(* *) +(* 2. 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. *) +(* *) +(* 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. *) +(* *) + (* This file contains the low-level proof rules for memory reads *) From self.low.rules Require Import prelude. diff --git a/theories/low/rules/reg.v b/theories/low/rules/reg.v index fe22ba8..918d26f 100644 --- a/theories/low/rules/reg.v +++ b/theories/low/rules/reg.v @@ -1,3 +1,39 @@ +(* *) +(* BSD 2-Clause License *) +(* *) +(* This applies to all files in this archive except folder *) +(* "system-semantics". *) +(* *) +(* Copyright (c) 2023, *) +(* Zongyuan Liu *) +(* Angus Hammond *) +(* Jean Pichon-Pharabod *) +(* Thibaut Pérami *) +(* *) +(* All rights reserved. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions are met: *) +(* *) +(* 1. Redistributions of source code must retain the above copyright notice, this *) +(* list of conditions and the following disclaimer. *) +(* *) +(* 2. 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. *) +(* *) +(* 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. *) +(* *) + (* This file contains the low-level proof rules for register operations *) From self.low.rules Require Import prelude. diff --git a/theories/low/rules/util.v b/theories/low/rules/util.v index 5126af8..a4a24f7 100644 --- a/theories/low/rules/util.v +++ b/theories/low/rules/util.v @@ -1,3 +1,39 @@ +(* *) +(* BSD 2-Clause License *) +(* *) +(* This applies to all files in this archive except folder *) +(* "system-semantics". *) +(* *) +(* Copyright (c) 2023, *) +(* Zongyuan Liu *) +(* Angus Hammond *) +(* Jean Pichon-Pharabod *) +(* Thibaut Pérami *) +(* *) +(* All rights reserved. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions are met: *) +(* *) +(* 1. Redistributions of source code must retain the above copyright notice, this *) +(* list of conditions and the following disclaimer. *) +(* *) +(* 2. 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. *) +(* *) +(* 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. *) +(* *) + (* This file contains the low-level proof rules for auxiliary operations *) From self.low.rules Require Import prelude. diff --git a/theories/low/rules/write.v b/theories/low/rules/write.v index d6fc6b9..37f3b13 100644 --- a/theories/low/rules/write.v +++ b/theories/low/rules/write.v @@ -1,3 +1,39 @@ +(* *) +(* BSD 2-Clause License *) +(* *) +(* This applies to all files in this archive except folder *) +(* "system-semantics". *) +(* *) +(* Copyright (c) 2023, *) +(* Zongyuan Liu *) +(* Angus Hammond *) +(* Jean Pichon-Pharabod *) +(* Thibaut Pérami *) +(* *) +(* All rights reserved. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions are met: *) +(* *) +(* 1. Redistributions of source code must retain the above copyright notice, this *) +(* list of conditions and the following disclaimer. *) +(* *) +(* 2. 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. *) +(* *) +(* 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. *) +(* *) + (* This file contains the low-level proof rules for (non-exclusive) memory writes *) From self.low.rules Require Import prelude. diff --git a/theories/low/rules/write_xcl.v b/theories/low/rules/write_xcl.v index 76c50af..31d66c3 100644 --- a/theories/low/rules/write_xcl.v +++ b/theories/low/rules/write_xcl.v @@ -1,3 +1,39 @@ +(* *) +(* BSD 2-Clause License *) +(* *) +(* This applies to all files in this archive except folder *) +(* "system-semantics". *) +(* *) +(* Copyright (c) 2023, *) +(* Zongyuan Liu *) +(* Angus Hammond *) +(* Jean Pichon-Pharabod *) +(* Thibaut Pérami *) +(* *) +(* All rights reserved. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions are met: *) +(* *) +(* 1. Redistributions of source code must retain the above copyright notice, this *) +(* list of conditions and the following disclaimer. *) +(* *) +(* 2. 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. *) +(* *) +(* 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. *) +(* *) + (* This file contains the low-level proof rules for exclusive memory writes *) From self.low.rules Require Import prelude. diff --git a/theories/low/weakestpre.v b/theories/low/weakestpre.v index ff6d30b..3adad94 100644 --- a/theories/low/weakestpre.v +++ b/theories/low/weakestpre.v @@ -1,3 +1,39 @@ +(* *) +(* BSD 2-Clause License *) +(* *) +(* This applies to all files in this archive except folder *) +(* "system-semantics". *) +(* *) +(* Copyright (c) 2023, *) +(* Zongyuan Liu *) +(* Angus Hammond *) +(* Jean Pichon-Pharabod *) +(* Thibaut Pérami *) +(* *) +(* All rights reserved. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions are met: *) +(* *) +(* 1. Redistributions of source code must retain the above copyright notice, this *) +(* list of conditions and the following disclaimer. *) +(* *) +(* 2. 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. *) +(* *) +(* 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. *) +(* *) + (* This file contains the definition of weakest preconditions of the low-level logic *) From iris.proofmode Require Import base tactics classes. From iris.bi.lib Require Import fixpoint. diff --git a/theories/middle/excl.v b/theories/middle/excl.v index 20a2c96..0438ba3 100644 --- a/theories/middle/excl.v +++ b/theories/middle/excl.v @@ -1,3 +1,39 @@ +(* *) +(* BSD 2-Clause License *) +(* *) +(* This applies to all files in this archive except folder *) +(* "system-semantics". *) +(* *) +(* Copyright (c) 2023, *) +(* Zongyuan Liu *) +(* Angus Hammond *) +(* Jean Pichon-Pharabod *) +(* Thibaut Pérami *) +(* *) +(* All rights reserved. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions are met: *) +(* *) +(* 1. Redistributions of source code must retain the above copyright notice, this *) +(* list of conditions and the following disclaimer. *) +(* *) +(* 2. 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. *) +(* *) +(* 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. *) +(* *) + (* This file includes the exclusive invariant and specialised rules *) (* From stdpp Require Import unstable.bitvector. *) diff --git a/theories/middle/instantiation.v b/theories/middle/instantiation.v index 00cdf4f..abedd4c 100644 --- a/theories/middle/instantiation.v +++ b/theories/middle/instantiation.v @@ -1,3 +1,39 @@ +(* *) +(* BSD 2-Clause License *) +(* *) +(* This applies to all files in this archive except folder *) +(* "system-semantics". *) +(* *) +(* Copyright (c) 2023, *) +(* Zongyuan Liu *) +(* Angus Hammond *) +(* Jean Pichon-Pharabod *) +(* Thibaut Pérami *) +(* *) +(* All rights reserved. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions are met: *) +(* *) +(* 1. Redistributions of source code must retain the above copyright notice, this *) +(* list of conditions and the following disclaimer. *) +(* *) +(* 2. 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. *) +(* *) +(* 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. *) +(* *) + (** This file contains the instantiation of the middle-level logic, this is the file that all helper files import*) From iris_named_props Require Export named_props. diff --git a/theories/middle/rules.v b/theories/middle/rules.v index daa4991..95f29d2 100644 --- a/theories/middle/rules.v +++ b/theories/middle/rules.v @@ -1,3 +1,39 @@ +(* *) +(* BSD 2-Clause License *) +(* *) +(* This applies to all files in this archive except folder *) +(* "system-semantics". *) +(* *) +(* Copyright (c) 2023, *) +(* Zongyuan Liu *) +(* Angus Hammond *) +(* Jean Pichon-Pharabod *) +(* Thibaut Pérami *) +(* *) +(* All rights reserved. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions are met: *) +(* *) +(* 1. Redistributions of source code must retain the above copyright notice, this *) +(* list of conditions and the following disclaimer. *) +(* *) +(* 2. 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. *) +(* *) +(* 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. *) +(* *) + (* This file lifts rules of the low-level logic to mid-level *) From stdpp.unstable Require Import bitvector bitvector_tactics. diff --git a/theories/middle/specialised_rules.v b/theories/middle/specialised_rules.v index 7386144..5c7d6e2 100644 --- a/theories/middle/specialised_rules.v +++ b/theories/middle/specialised_rules.v @@ -1,3 +1,39 @@ +(* *) +(* BSD 2-Clause License *) +(* *) +(* This applies to all files in this archive except folder *) +(* "system-semantics". *) +(* *) +(* Copyright (c) 2023, *) +(* Zongyuan Liu *) +(* Angus Hammond *) +(* Jean Pichon-Pharabod *) +(* Thibaut Pérami *) +(* *) +(* All rights reserved. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions are met: *) +(* *) +(* 1. Redistributions of source code must retain the above copyright notice, this *) +(* list of conditions and the following disclaimer. *) +(* *) +(* 2. 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. *) +(* *) +(* 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. *) +(* *) + (* This file contains some highly specialised mid-level proof rules (mostly for loads and stores) *) From stdpp.unstable Require Import bitvector bitvector_tactics. diff --git a/theories/middle/weakestpre.v b/theories/middle/weakestpre.v index c95972f..3a8e5ea 100644 --- a/theories/middle/weakestpre.v +++ b/theories/middle/weakestpre.v @@ -1,3 +1,39 @@ +(* *) +(* BSD 2-Clause License *) +(* *) +(* This applies to all files in this archive except folder *) +(* "system-semantics". *) +(* *) +(* Copyright (c) 2023, *) +(* Zongyuan Liu *) +(* Angus Hammond *) +(* Jean Pichon-Pharabod *) +(* Thibaut Pérami *) +(* *) +(* All rights reserved. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions are met: *) +(* *) +(* 1. Redistributions of source code must retain the above copyright notice, this *) +(* list of conditions and the following disclaimer. *) +(* *) +(* 2. 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. *) +(* *) +(* 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. *) +(* *) + (** This file contains the instantiation of the middle-level logic, this is the file that all helper files import*) From iris_named_props Require Export named_props. diff --git a/theories/stdpp_extra.v b/theories/stdpp_extra.v index ab77e8d..f0b44a5 100644 --- a/theories/stdpp_extra.v +++ b/theories/stdpp_extra.v @@ -1,3 +1,39 @@ +(* *) +(* BSD 2-Clause License *) +(* *) +(* This applies to all files in this archive except folder *) +(* "system-semantics". *) +(* *) +(* Copyright (c) 2023, *) +(* Zongyuan Liu *) +(* Angus Hammond *) +(* Jean Pichon-Pharabod *) +(* Thibaut Pérami *) +(* *) +(* All rights reserved. *) +(* *) +(* Redistribution and use in source and binary forms, with or without *) +(* modification, are permitted provided that the following conditions are met: *) +(* *) +(* 1. Redistributions of source code must retain the above copyright notice, this *) +(* list of conditions and the following disclaimer. *) +(* *) +(* 2. 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. *) +(* *) +(* 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. *) +(* *) + From stdpp Require Import ssreflect list sets fin_maps fin_map_dom gmap. Lemma head_app{A} (l1 l2 :list A): head (l1 ++ l2) = match head l1 with