Skip to content

Commit

Permalink
Add license header to all Coq files
Browse files Browse the repository at this point in the history
  • Loading branch information
@lzy0505
lzy0505 committed Nov 13, 2023
1 parent b24deb7 commit 1cd1034
Show file tree
Hide file tree
Showing 60 changed files with 2,193 additions and 0 deletions.
38 changes: 38 additions & 0 deletions system-semantics/Common/CBase.v
View file
Original file line number Diff line number Diff line change
@@ -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.
Expand Down
39 changes: 39 additions & 0 deletions system-semantics/Common/CBitvector.v
View file
Original file line number Diff line number Diff line change
@@ -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 *)

Expand Down
39 changes: 39 additions & 0 deletions system-semantics/Common/CBool.v
View file
Original file line number Diff line number Diff line change
@@ -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.
Expand Down
39 changes: 39 additions & 0 deletions system-semantics/Common/CInduction.v
View file
Original file line number Diff line number Diff line change
@@ -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.
Expand Down
39 changes: 39 additions & 0 deletions system-semantics/Common/CList.v
View file
Original file line number Diff line number Diff line change
@@ -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.
Expand Down
39 changes: 39 additions & 0 deletions system-semantics/Common/CMaps.v
View file
Original file line number Diff line number Diff line change
@@ -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.

Expand Down
Loading

0 comments on commit 1cd1034

Please sign in to comment.